1  /-
  2  Copyright (c) 2018 Kenny Lau. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Kenny Lau
  5  
  6  Free groups as a quotient over the reduction relation `a * x * x⁻¹ * b = a * b`.
  7  
  8  First we introduce the one step reduction relation
  9    `free_group.red.step`:  w * x * x⁻¹ * v   ~>   w * v
 10  its reflexive transitive closure:
 11    `free_group.red.trans`
 12  and proof that its join is an equivalence relation.
 13  
 14  Then we introduce `free_group α` as a quotient over `free_group.red.step`.
 15  -/
 16  import logic.relation
src         └────────────┘
 17  import algebra.group algebra.group_power
src         └───────────┘ └─────────────────┘
 18  import data.fintype data.list.basic
src         └──────────┘ └─────────────┘
 19  import group_theory.subgroup
src         └───────────────────┘
 20  open relation
 21  
 22  universes u v w
 23  
 24  variables {α : Type u}
id             
typ            
 25  
 26  local attribute [simp] list.append_eq_has_append
id                          └───────────────────────┘
src                         └───────────────────────┘
typ                         └───────────────────────┘
doc                   └──┘
 27  
 28  namespace free_group
 29  variables {L L₁ L₂ L₃ L₄ : list (α × bool)}
id                              └──┘     └──┘
src                             └──┘     └──┘
typ                             └──┘     └──┘
 30  
 31  /-- Reduction step: `w * x * x⁻¹ * v ~> w * v` -/
 32  inductive red.step : list (α × bool) → list (α × bool) → Prop
id                        └──┘     └──┘    └──┘     └──┘
src                       └──┘     └──┘    └──┘     └──┘
typ                       └──┘     └──┘    └──┘     └──┘
 33  | bnot {L₁ L₂ x b} : red.step (L₁ ++ (x, b) :: (x, bnot b) :: L₂) (L₁ ++ L₂)
id           └┘ └┘                └┘ └┘     └┘   └──┘   └┘ └┘   └┘ └┘ └┘
src                                    └┘       └┘    └──┘    └┘         └┘
typ          └┘ └┘                └┘ └┘     └┘   └──┘   └┘ └┘   └┘ └┘ └┘
 34  attribute [simp] red.step.bnot
id                    └───────────┘
src                   └───────────┘
typ                   └───────────┘
doc             └──┘
 35  
 36  /-- Reflexive-transitive closure of red.step -/
 37  def red : list (α × bool) → list (α × bool) → Prop := refl_trans_gen red.step
id             └──┘    └──┘    └──┘    └──┘            └────────────┘ └──────┘
src            └──┘     └──┘    └──┘     └──┘            └────────────┘ └──────┘
typ            └──┘    └──┘    └──┘    └──┘            └────────────┘ └──────┘
doc                                                        └────────────┘ └──────┘
 38  
 39  @[refl] lemma red.refl : red L L := refl_trans_gen.refl
id                            └─┘      └─────────────────┘
src    └──┘                   └─┘        └─────────────────┘
typ                           └─┘      └─────────────────┘
doc    └──┘                   └─┘
 40  @[trans] lemma red.trans : red L₁ L₂ → red L₂ L₃ → red L₁ L₃ := refl_trans_gen.trans
id                              └─┘ └┘ └┘   └─┘ └┘ └┘   └─┘ └┘ └┘    └──────────────────┘
src    └───┘                    └─┘         └─┘         └─┘          └──────────────────┘
typ                             └─┘ └┘ └┘   └─┘ └┘ └┘   └─┘ └┘ └┘    └──────────────────┘
doc    └───┘                    └─┘         └─┘         └─┘
 41  
 42  namespace red
 43  
 44  /-- Predicate asserting that word `w₁` can be reduced to `w₂` in one step, i.e. there are words
 45  `w₃ w₄` and letter `x` such that `w₁ = w₃xx⁻¹w₄` and `w₂ = w₃w₄`  -/
 46  theorem step.length : ∀ {L₁ L₂ : list (α × bool)}, step L₁ L₂ → L₂.length + 2 = L₁.length
id                                   └──┘    └──┘    └──┘ └┘ └┘   └┘└─────┘     └┘└─────┘
src                                   └──┘     └──┘    └──┘           └─────┘       └─────┘
typ                                  └──┘    └──┘    └──┘ └┘ └┘   └┘└─────┘     └┘└─────┘
doc                                                     └──┘
 47  | _ _ (@red.step.bnot _ L1 L2 x b) := by rw [list.length_append, list.length_append]; refl
id           └───────────┘                        └────────────────┘  └────────────────┘
src          └───────────┘                    └──┘└────────────────┘└┘└────────────────┘  └────
typ          └───────────┘                    └──┘└────────────────┘└┘└────────────────┘  └────
doc                                           └──┘                  └┘                    └────
txt                                           └──┘                  └┘                    └────
par                                           └──┘                  └┘                    └────
pid                                             └┘                  └┘                        
st                                           └─────────────────────┘└──────────────────┘└──────
 48  
src  
typ  
doc  
txt  
par  
pid  
st   
 49  @[simp] lemma step.bnot_rev {x b} : step (L₁ ++ (x, bnot b) :: (x, b) :: L₂) (L₁ ++ L₂) :=
id                                       └──┘  └┘ └┘   └──┘   └┘     └┘ └┘   └┘ └┘ └┘
src                                      └──┘     └┘    └──┘    └┘       └┘         └┘
typ                                      └──┘  └┘ └┘   └──┘   └┘     └┘ └┘   └┘ └┘ └┘
doc    └──┘                              └──┘
 50  by cases b; from step.bnot
id                   └───────┘
src     └────┘   └───┘└───────┘
typ     └────┘  └───┘└───────┘
doc     └────┘   └───┘         
txt     └────┘   └───┘         
par     └────┘   └───┘         
pid             └───┘         
st     └────────────────────────
 51  
src  
typ  
doc  
txt  
par  
pid  
st   
 52  @[simp] lemma step.cons_bnot {x b} : red.step ((x, b) :: (x, bnot b) :: L) L :=
id                                        └──────┘      └┘   └──┘   └┘   
src                                       └──────┘        └┘    └──┘    └┘
typ                                       └──────┘      └┘   └──┘   └┘   
doc    └──┘                               └──────┘
 53  @step.bnot _ [] _ _ _
id    └───────┘   └┘
src   └───────┘   └┘
typ   └───────┘   └┘
 54  
 55  @[simp] lemma step.cons_bnot_rev {x b} : red.step ((x, bnot b) :: (x, b) :: L) L :=
id                                            └──────┘    └──┘   └┘     └┘   
src                                           └──────┘     └──┘    └┘       └┘
typ                                           └──────┘    └──┘   └┘     └┘   
doc    └──┘                                   └──────┘
 56  @red.step.bnot_rev _ [] _ _ _
id    └───────────────┘   └┘
src   └───────────────┘   └┘
typ   └───────────────┘   └┘
 57  
 58  theorem step.append_left : ∀ {L₁ L₂ L₃ : list (α × bool)}, step L₂ L₃ → step (L₁ ++ L₂) (L₁ ++ L₃)
id                                           └──┘    └──┘    └──┘ └┘ └┘   └──┘  └┘ └┘ └┘   └┘ └┘ └┘
src                                           └──┘     └──┘    └──┘         └──┘     └┘         └┘
typ                                          └──┘    └──┘    └──┘ └┘ └┘   └──┘  └┘ └┘ └┘   └┘ └┘ └┘
doc                                                             └──┘         └──┘
 59  | _ _ _ red.step.bnot := by rw [← list.append_assoc, ← list.append_assoc]; constructor
id           └───────────┘             └───────────────┘    └───────────────┘
src          └───────────┘       └────┘└───────────────┘└──┘└───────────────┘  └───────────
typ          └───────────┘       └────┘└───────────────┘└──┘└───────────────┘  └───────────
doc                              └────┘                 └──┘                   └───────────
txt                              └────┘                 └──┘                   └───────────
par                              └────┘                 └──┘                   └───────────
pid                                └──┘                 └──┘                              
st                              └──────────────────────┘└───────────────────┘└─────────────
 60  
src  
typ  
doc  
txt  
par  
pid  
st   
 61  theorem step.cons {x} (H : red.step L₁ L₂) : red.step (x :: L₁) (x :: L₂) :=
id                              └──────┘ └┘ └┘    └──────┘   └┘ └┘    └┘ └┘
src                             └──────┘          └──────┘    └┘        └┘
typ                             └──────┘ └┘ └┘    └──────┘   └┘ └┘    └┘ └┘
doc                             └──────┘          └──────┘
 62  @step.append_left _ [x] _ _ H
id    └──────────────┘        
src   └──────────────┘    
typ   └──────────────┘        
 63  
 64  theorem step.append_right : ∀ {L₁ L₂ L₃ : list (α × bool)}, step L₁ L₂ → step (L₁ ++ L₃) (L₂ ++ L₃)
id                                            └──┘    └──┘    └──┘ └┘ └┘   └──┘  └┘ └┘ └┘   └┘ └┘ └┘
src                                            └──┘     └──┘    └──┘         └──┘     └┘         └┘
typ                                           └──┘    └──┘    └──┘ └┘ └┘   └──┘  └┘ └┘ └┘   └┘ └┘ └┘
doc                                                              └──┘         └──┘
 65  | _ _ _ red.step.bnot := by simp
id           └───────────┘
src          └───────────┘       └────
typ          └───────────┘       └────
doc                              └────
txt                              └────
par                              └────
pid                                  
st                              └─────
 66  
src  
typ  
doc  
txt  
par  
pid  
st   
 67  lemma not_step_nil : ¬ step [] L :=
id                         └──┘ └┘ 
src                        └──┘ └┘
typ                        └──┘ └┘ 
doc                         └──┘
 68  begin
st   └─────
 69    generalize h' : [] = L',
id                     └┘
src    └──────────────┘└┘ 
typ    └──────────────┘└┘ 
doc    └──────────────┘   
txt    └──────────────┘   
par    └──────────────┘   
pid              └─┘└┘   
st   ────────────────────────┘└─
 70    assume h,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
 71    cases h with L₁ L₂,
id           
src    └────┘ └─────────┘
typ    └────┘└─────────┘
doc    └────┘ └─────────┘
txt    └────┘ └─────────┘
par    └────┘ └─────────┘
pid          └─────────┘
st   ───────────────────┘└─
 72    simp [list.nil_eq_append_iff] at h',
id           └────────────────────┘
src    └────┘└────────────────────┘└─────┘
typ    └────┘└────────────────────┘└─────┘
doc    └────┘                      └─────┘
txt    └────┘                      └─────┘
par    └────┘                      └─────┘
pid                              └───┘
st   ────────────────────────────────────┘└─
 73    contradiction
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid                 
st   ───────────────┘
 74  end
st   └─┘
 75  
 76  lemma step.cons_left_iff {a : α} {b : bool} :
id                                        └──┘
src                                        └──┘
typ                                       └──┘
 77    step ((a, b) :: L₁) L₂ ↔ (∃L, step L₁ L ∧ L₂ = (a, b) :: L) ∨ (L₁ = (a, bnot b)::L₂) :=
id     └──┘      └┘ └┘  └┘    └──┘ └┘   └┘      └┘     └┘    └──┘  └┘└┘
src    └──┘        └┘            └──┘                 └┘             └──┘   └┘
typ    └──┘      └┘ └┘  └┘    └──┘ └┘   └┘      └┘     └┘    └──┘  └┘└┘
doc    └──┘                          └──┘
 78  begin
st   └─────
 79    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
 80    { generalize hL : ((a, b) :: L₁ : list _) = L,
id                               └┘   └──┘
src      └──────────────┘  └┘ └┘    └─┘└──┘└──┘ 
typ      └──────────────┘ └┘└┘  └┘└─┘└──┘└──┘ 
doc      └──────────────┘   └┘ └┘    └─┘    └──┘ 
txt      └──────────────┘   └┘ └┘    └─┘    └──┘ 
par      └──────────────┘   └┘ └┘    └─┘    └──┘ 
pid                └─┘└┘   └┘ └┘    └─┘    └──┘ 
st   ───┘└─────────────────────────────────────────┘└─
 81      assume h,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
 82      rcases h with ⟨_ | ⟨p, s'⟩, e, a', b'⟩,
id              
src      └─────┘ └────────────────────────────┘
typ      └─────┘└────────────────────────────┘
doc      └─────┘ └────────────────────────────┘
txt      └─────┘ └────────────────────────────┘
par      └─────┘ └────────────────────────────┘
pid             └────────────────────────────┘
st   ─────────────────────────────────────────┘└─
 83      { simp at hL, simp [*] },
src        └────────┘  └───────┘
typ        └────────┘  └───────┘
doc        └────────┘  └───────┘
txt        └────────┘  └───────┘
par        └────────┘  └───────┘
pid            └───┘      └─┘
st   ─────┘└────────┘└─────────┘└┘
 84      { simp at hL,
src        └────────┘
typ        └────────┘
doc        └────────┘
txt        └────────┘
par        └────────┘
pid            └───┘
st   ───────────────┘└─
 85        rcases hL with ⟨rfl, rfl⟩,
id                └┘
src        └─────┘  └──────────────┘
typ        └─────┘└┘└──────────────┘
doc        └─────┘  └──────────────┘
txt        └─────┘  └──────────────┘
par        └─────┘  └──────────────┘
pid                └──────────────┘
st   ──────────────────────────────┘└─
 86        refine or.inl ⟨s' ++ e, step.bnot, _⟩,
id                └────┘  └┘ └┘   └───────┘
src        └─────┘└────┘   └┘ └┘└───────┘└──┘
typ        └─────┘└────┘ └┘└┘└┘└───────┘└──┘
doc        └─────┘            └┘         └──┘
txt        └─────┘            └┘         └──┘
par        └─────┘            └┘         └──┘
pid                          └┘         └──┘
st   ──────────────────────────────────────────┘└─
 87        simp } },
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid            
st   ──────────┘└──┘
 88    { assume h,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
 89      rcases h with ⟨L, h, rfl⟩ | rfl,
id              
src      └─────┘ └─────────────────────┘
typ      └─────┘└─────────────────────┘
doc      └─────┘ └─────────────────────┘
txt      └─────┘ └─────────────────────┘
par      └─────┘ └─────────────────────┘
pid             └─────────────────────┘
st   ──────────────────────────────────┘└─
 90      { exact step.cons h },
id               └───────┘ 
src        └────┘└───────┘ 
typ        └────┘└───────┘
doc        └────┘          
txt        └────┘          
par        └────┘          
pid                       
st   ─────┘└────────────────┘└┘
 91      { exact step.cons_bnot } }
id               └────────────┘
src        └────┘└────────────┘
typ        └────┘└────────────┘
doc        └────┘              
txt        └────┘              
par        └────┘              
pid                           
st   ──────────────────────────┘└───
 92  end
st   ──┘
 93  
 94  lemma not_step_singleton : ∀ {p : α × bool}, ¬ step [p] L
id                                      └──┘    └──┘  
src                                       └──┘    └──┘  
typ                                     └──┘    └──┘  
doc                                                 └──┘
 95  | (a, b) := by simp [step.cons_left_iff, not_step_nil]
id                       └────────────────┘  └──────────┘
src                └────┘└────────────────┘└┘└──────────┘└─
typ                └────┘└────────────────┘└┘└──────────┘└─
doc                 └────┘                  └┘            └─
txt                 └────┘                  └┘            └─
par                 └────┘                  └┘            └─
pid                                       └┘            
st                 └────────────────────────────────────────
 96  
src  
typ  
doc  
txt  
par  
pid  
st   
 97  lemma step.cons_cons_iff : ∀{p : α × bool}, step (p :: L₁) (p :: L₂) ↔ step L₁ L₂ :=
id                                      └──┘   └──┘   └┘ └┘    └┘ └┘   └──┘ └┘ └┘
src                                      └──┘   └──┘    └┘        └┘      └──┘
typ                                     └──┘   └──┘   └┘ └┘    └┘ └┘   └──┘ └┘ └┘
doc                                              └──┘                       └──┘
 98  by simp [step.cons_left_iff, iff_def, or_imp_distrib] {contextual := tt}
id            └────────────────┘  └─────┘  └────────────┘                 └┘
src     └────┘└────────────────┘└┘└─────┘└┘└────────────┘└┘ └────────────┘└┘└─
typ     └────┘└────────────────┘└┘└─────┘└┘└────────────┘└┘ └────────────┘└┘└─
doc     └────┘                  └┘       └┘              └┘ └────────────┘  └─
txt     └────┘                  └┘       └┘              └┘ └────────────┘  └─
par     └────┘                  └┘       └┘              └┘ └────────────┘  └─
pid                           └┘       └┘               └────────────┘  
st     └──────────────────────────────────────────────────────────────────────
 99  
src  
typ  
doc  
txt  
par  
pid  
st   
100  lemma step.append_left_iff : ∀L, step (L ++ L₁) (L ++ L₂) ↔ step L₁ L₂
id                                   └──┘   └┘ └┘    └┘ └┘   └──┘ └┘ └┘
src                                   └──┘    └┘        └┘      └──┘
typ                                  └──┘   └┘ └┘    └┘ └┘   └──┘ └┘ └┘
doc                                   └──┘                       └──┘
101  | [] := by simp
id     └┘
src    └┘       └───┘
typ    └┘       └───┘
doc             └───┘
txt             └───┘
par             └───┘
pid                 
st             └────┘
102  | (p :: l) := by simp [step.append_left_iff l, step.cons_cons_iff]
id        └┘                └──────────────────┘   └────────────────┘
src       └┘          └────┘                     └┘└────────────────┘└─
typ       └┘          └────┘└──────────────────┘└┘└────────────────┘└─
doc                   └────┘                     └┘                  └─
txt                   └────┘                     └┘                  └─
par                   └────┘                     └┘                  └─
pid                                            └┘                  
st                   └──────────────────────────────────────────────────
103  
src  
typ  
doc  
txt  
par  
pid  
st   
104  private theorem step.diamond_aux : ∀ {L₁ L₂ L₃ L₄ : list (α × bool)} {x1 b1 x2 b2},
id                                                      └──┘    └──┘    └┘ └┘ └┘ └┘
src                                                      └──┘     └──┘
typ                                                     └──┘    └──┘    └┘ └┘ └┘ └┘
105    L₁ ++ (x1, b1) :: (x1, bnot b1) :: L₂ = L₃ ++ (x2, b2) :: (x2, bnot b2) :: L₄ →
id     └┘ └┘ └┘  └┘  └┘ └┘  └──┘ └┘  └┘ └┘  └┘ └┘ └┘  └┘  └┘ └┘  └──┘ └┘  └┘ └┘
src       └┘         └┘     └──┘     └┘        └┘         └┘     └──┘     └┘
typ    └┘ └┘ └┘  └┘  └┘ └┘  └──┘ └┘  └┘ └┘  └┘ └┘ └┘  └┘  └┘ └┘  └──┘ └┘  └┘ └┘
106    L₁ ++ L₂ = L₃ ++ L₄ ∨ ∃ L₅, red.step (L₁ ++ L₂) L₅ ∧ red.step (L₃ ++ L₄) L₅
id     └┘ └┘ └┘  └┘ └┘ └┘   └┘ └──────┘  └┘ └┘ └┘  └┘  └──────┘  └┘ └┘ └┘  └┘
src       └┘        └┘         └──────┘     └┘         └──────┘     └┘
typ    └┘ └┘ └┘  └┘ └┘ └┘   └┘ └──────┘  └┘ └┘ └┘  └┘  └──────┘  └┘ └┘ └┘  └┘
doc                                └──────┘                 └──────┘
107  | []        _ []        _ _ _ _ _ H := by injections; subst_vars; simp
id     └┘          └┘
src    └┘          └┘                          └────────┘  └────────┘  └───┘
typ    └┘          └┘                          └────────┘  └────────┘  └───┘
doc                                            └────────┘  └────────┘  └───┘
txt                                            └────────┘  └────────┘  └───┘
par                                            └────────┘  └────────┘  └───┘
pid                                                                        
st                                            └────────────────────────────┘
108  | []        _ [(x3,b3)] _ _ _ _ _ H := by injections; subst_vars; simp
id     └┘                
src    └┘                                   └────────┘  └────────┘  └───┘
typ    └┘                                   └────────┘  └────────┘  └───┘
doc                                            └────────┘  └────────┘  └───┘
txt                                            └────────┘  └────────┘  └───┘
par                                            └────────┘  └────────┘  └───┘
pid                                                                        
st                                            └────────────────────────────┘
109  | [(x3,b3)] _ []        _ _ _ _ _ H := by injections; subst_vars; simp
id              └┘
src             └┘                          └────────┘  └────────┘  └───┘
typ             └┘                          └────────┘  └────────┘  └───┘
doc                                            └────────┘  └────────┘  └───┘
txt                                            └────────┘  └────────┘  └───┘
par                                            └────────┘  └────────┘  └───┘
pid                                                                        
st                                            └────────────────────────────┘
110  | []                     _ ((x3,b3)::(x4,b4)::tl) _ _ _ _ _ H :=
id     └┘                              └┘      └┘
src    └┘                              └┘      └┘
typ    └┘                              └┘      └┘
111    by injections; subst_vars; simp; right; exact ⟨_, red.step.bnot, red.step.cons_bnot⟩
id                                                       └───────────┘  └────────────────┘
src       └────────┘  └────────┘  └──┘  └───┘  └────┘ └─┘└───────────┘└┘└────────────────┘└┘
typ       └────────┘  └────────┘  └──┘  └───┘  └────┘ └─┘└───────────┘└┘└────────────────┘└┘
doc       └────────┘  └────────┘  └──┘  └───┘  └────┘ └─┘             └┘                  └┘
txt       └────────┘  └────────┘  └──┘  └───┘  └────┘ └─┘             └┘                  └┘
par       └────────┘  └────────┘  └──┘  └───┘  └────┘ └─┘             └┘                  └┘
pid                                                  └─┘             └┘                  
st       └─────────────────────────────────────────────────────────────────────────────────┘
112  | ((x3,b3)::(x4,b4)::tl) _ []                     _ _ _ _ _ H :=
id            └┘      └┘      └┘
src           └┘      └┘      └┘
typ           └┘      └┘      └┘
113    by injections; subst_vars; simp; right; exact ⟨_, red.step.cons_bnot, red.step.bnot⟩
id                                                       └────────────────┘  └───────────┘
src       └────────┘  └────────┘  └──┘  └───┘  └────┘ └─┘└────────────────┘└┘└───────────┘└┘
typ       └────────┘  └────────┘  └──┘  └───┘  └────┘ └─┘└────────────────┘└┘└───────────┘└┘
doc       └────────┘  └────────┘  └──┘  └───┘  └────┘ └─┘                  └┘             └┘
txt       └────────┘  └────────┘  └──┘  └───┘  └────┘ └─┘                  └┘             └┘
par       └────────┘  └────────┘  └──┘  └───┘  └────┘ └─┘                  └┘             └┘
pid                                                  └─┘                  └┘             
st       └─────────────────────────────────────────────────────────────────────────────────┘
114  | ((x3,b3)::tl) _ ((x4,b4)::tl2) _ _ _ _ _ H :=
id            └┘             └┘               
src           └┘             └┘
typ           └┘             └┘               
115    let ⟨H1, H2⟩ := list.cons.inj H in
id     └─┘      └┘     └───────────┘
src                    └───────────┘
typ    └─┘      └┘     └───────────┘
116    match step.diamond_aux H2 with
id           └──────────────┘
typ          └──────────────┘
117      | or.inl H3 := or.inl $ by simp [H1, H3]
id         └────┘       └────┘            └┘  └┘
src        └────┘       └────┘      └────┘  └┘  └─
typ        └────┘       └────┘      └────┘└┘└┘└┘└─
doc                                 └────┘  └┘  └─
txt                                 └────┘  └┘  └─
par                                 └────┘  └┘  └─
pid                                       └┘  
st                                 └──────────────
118      | or.inr ⟨L₅, H3, H4⟩ := or.inr
id         └────┘      └┘         └────┘
src  ───┘  └────┘                 └────┘
typ  ───┘  └────┘      └┘         └────┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘
119        ⟨_, step.cons H3, by simpa [H1] using step.cons H4⟩
id             └───────┘               └┘        └───────┘ └┘
src            └───────┘        └─────┘  └──────┘└───────┘
typ            └───────┘        └─────┘└┘└──────┘└───────┘└┘
doc                             └─────┘  └──────┘         
txt                             └─────┘  └──────┘         
par                             └─────┘  └──────┘         
pid                                    └────┘         
st                             └────────────────────────────┘
120    end
121  
122  theorem step.diamond : ∀ {L₁ L₂ L₃ L₄ : list (α × bool)},
id                                          └──┘    └──┘
src                                          └──┘     └──┘
typ                                         └──┘    └──┘
123    red.step L₁ L₃ → red.step L₂ L₄ → L₁ = L₂ →
id     └──────┘ └┘ └┘   └──────┘ └┘ └┘   └┘  └┘
src    └──────┘         └──────┘            
typ    └──────┘ └┘ └┘   └──────┘ └┘ └┘   └┘  └┘
doc    └──────┘         └──────┘
124    L₃ = L₄ ∨ ∃ L₅, red.step L₃ L₅ ∧ red.step L₄ L₅
id     └┘  └┘   └┘ └──────┘ └┘ └┘  └──────┘ └┘ └┘
src                └──────┘        └──────┘
typ    └┘  └┘   └┘ └──────┘ └┘ └┘  └──────┘ └┘ └┘
doc                    └──────┘         └──────┘
125  | _ _ _ _ red.step.bnot red.step.bnot H := step.diamond_aux H
id                           └───────────┘     └──────────────┘
src                          └───────────┘      └──────────────┘
typ                          └───────────┘     └──────────────┘
126  
127  lemma step.to_red : step L₁ L₂ → red L₁ L₂ :=
id                       └──┘ └┘ └┘   └─┘ └┘ └┘
src                      └──┘         └─┘
typ                      └──┘ └┘ └┘   └─┘ └┘ └┘
doc                      └──┘         └─┘
128  refl_trans_gen.single
id   └───────────────────┘
src  └───────────────────┘
typ  └───────────────────┘
129  
130  /-- Church-Rosser theorem for word reduction: If `w1 w2 w3` are words such that `w1` reduces to `w2`
131  and `w3` respectively, then there is a word `w4` such that `w2` and `w3` reduce to `w4` respectively. -/
132  theorem church_rosser : red L₁ L₂ → red L₁ L₃ → join red L₂ L₃ :=
id                           └─┘ └┘ └┘   └─┘ └┘ └┘   └──┘ └─┘ └┘ └┘
src                          └─┘         └─┘         └──┘ └─┘
typ                          └─┘ └┘ └┘   └─┘ └┘ └┘   └──┘ └─┘ └┘ └┘
doc                          └─┘         └─┘              └─┘
133  relation.church_rosser (assume a b c hab hac,
id   └────────────────────┘            └─┘ └─┘
src  └────────────────────┘
typ  └────────────────────┘            └─┘ └─┘
134  match b, c, red.step.diamond hab hac rfl with
id             └──────────────┘ └─┘ └─┘ └─┘
src              └──────────────┘         └─┘
typ            └──────────────┘ └─┘ └─┘ └─┘
135  | b, _, or.inl rfl           := ⟨b, by refl, by refl⟩
id          └────┘ └─┘
src          └────┘ └─┘                     └──┘     └──┘
typ         └────┘ └─┘                     └──┘     └──┘
doc                                         └──┘     └──┘
txt                                         └──┘     └──┘
par                                         └──┘     └──┘
st                                         └───┘    └───┘
136  | b, c, or.inr ⟨d, hbd, hcd⟩ := ⟨d, refl_gen.single hbd, hcd.to_red⟩
id           └────┘    └─┘  └─┘         └─────────────┘         └─────┘
src          └────┘                      └─────────────┘         └─────┘
typ          └────┘    └─┘  └─┘         └─────────────┘         └─────┘
137  end)
138  
139  lemma cons_cons {p} : red L₁ L₂ → red (p :: L₁) (p :: L₂) :=
id                         └─┘ └┘ └┘   └─┘   └┘ └┘    └┘ └┘
src                        └─┘         └─┘    └┘        └┘
typ                        └─┘ └┘ └┘   └─┘   └┘ └┘    └┘ └┘
doc                        └─┘         └─┘
140  refl_trans_gen_lift (list.cons p) (assume a b, step.cons)
id   └─────────────────┘  └───────┘              └───────┘
src  └─────────────────┘  └───────┘                 └───────┘
typ  └─────────────────┘  └───────┘              └───────┘
141  
142  lemma cons_cons_iff (p) : red (p :: L₁) (p :: L₂) ↔ red L₁ L₂ :=
id                             └─┘   └┘ └┘    └┘ └┘   └─┘ └┘ └┘
src                            └─┘    └┘        └┘      └─┘
typ                            └─┘   └┘ └┘    └┘ └┘   └─┘ └┘ └┘
doc                            └─┘                       └─┘
143  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
144    begin
st     └─────
145      generalize eq₁ : (p :: L₁ : list _) = LL₁,
id                             └┘   └──┘
src      └───────────────┘      └─┘└──┘└──┘ 
typ      └───────────────┘   └┘└─┘└──┘└──┘ 
doc      └───────────────┘      └─┘    └──┘ 
txt      └───────────────┘      └─┘    └──┘ 
par      └───────────────┘      └─┘    └──┘ 
pid                └──┘└┘      └─┘    └──┘ 
st   ────────────────────────────────────────────┘└─
146      generalize eq₂ : (p :: L₂ : list _) = LL₂,
id                             └┘   └──┘
src      └───────────────┘      └─┘└──┘└──┘ 
typ      └───────────────┘   └┘└─┘└──┘└──┘ 
doc      └───────────────┘      └─┘    └──┘ 
txt      └───────────────┘      └─┘    └──┘ 
par      └───────────────┘      └─┘    └──┘ 
pid                └──┘└┘      └─┘    └──┘ 
st   ────────────────────────────────────────────┘└─
147      assume h,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
148      induction h using relation.refl_trans_gen.head_induction_on
id                 
src      └────────┘ └────────────────────────────────────────────────
typ      └────────┘└────────────────────────────────────────────────
doc      └────────┘ └────────────────────────────────────────────────
txt      └────────┘ └────────────────────────────────────────────────
par      └────────┘ └────────────────────────────────────────────────
pid                └──────────────────────────────────────────────┘
st   ────────────────────────────────────────────────────────────────
149        with L₁ L₂ h₁₂ h ih
src  ──────────────────────────
typ  ──────────────────────────
doc  ──────────────────────────
txt  ──────────────────────────
par  ──────────────────────────
pid  ────────────────────────┘
st   ──────────────────────────
150        generalizing L₁ L₂,
src  ───────────────────────┘
typ  ───────────────────────┘
doc  ───────────────────────┘
txt  ───────────────────────┘
par  ───────────────────────┘
pid  ───────────────────────┘
st   ───────────────────────┘└─
151      { subst_vars, cases eq₂, constructor },
id                           └─┘
src        └────────┘  └────┘     └──────────┘
typ        └────────┘  └────┘└─┘  └──────────┘
doc        └────────┘  └────┘     └──────────┘
txt        └────────┘  └────┘     └──────────┘
par        └────────┘  └────┘     └──────────┘
pid                                         
st   ─────┘└────────┘└─────────┘└────────────┘└┘
152      { subst_vars,
src        └────────┘
typ        └────────┘
doc        └────────┘
txt        └────────┘
par        └────────┘
st   ───────────────┘└─
153        cases p with a b,
id               
src        └────┘ └───────┘
typ        └────┘└───────┘
doc        └────┘ └───────┘
txt        └────┘ └───────┘
par        └────┘ └───────┘
pid              └───────┘
st   ─────────────────────┘└─
154        rw [step.cons_left_iff] at h₁₂,
id             └────────────────┘
src        └──┘└────────────────┘└──────┘
typ        └──┘└────────────────┘└──────┘
doc        └──┘                  └──────┘
txt        └──┘                  └──────┘
par        └──┘                  └──────┘
pid          └┘                  └─────┘
st   ───────────────────────────┘└─────┘└─
155        rcases h₁₂ with ⟨L, h₁₂, rfl⟩ | rfl,
id                └─┘
src        └─────┘   └───────────────────────┘
typ        └─────┘└─┘└───────────────────────┘
doc        └─────┘   └───────────────────────┘
txt        └─────┘   └───────────────────────┘
par        └─────┘   └───────────────────────┘
pid                 └───────────────────────┘
st   ────────────────────────────────────────┘└─
156        { exact (ih rfl rfl).head h₁₂ },
id                  └┘     └─┘       └─┘
src          └────┘      └─┘└─────┘   
typ          └────┘ └┘   └─┘└─────┘└─┘
doc          └────┘         └─────┘   
txt          └────┘         └─────┘   
par          └────┘         └─────┘   
pid                        └─────┘   
st   ───────┘└──────────────────────────┘└┘
157        { exact (cons_cons h).tail step.cons_bnot_rev } }
id                  └───────┘        └────────────────┘
src          └────┘ └───────┘ └─────┘└────────────────┘
typ          └────┘ └───────┘└─────┘└────────────────┘
doc          └────┘           └─────┘                  
txt          └────┘           └─────┘                  
par          └────┘           └─────┘                  
pid                          └─────┘                  
st   ───────────────────────────────────────────────────┘└───
158    end
st   ────┘
159    cons_cons
id     └───────┘
src    └───────┘
typ    └───────┘
160  
161  lemma append_append_left_iff : ∀L, red (L ++ L₁) (L ++ L₂) ↔ red L₁ L₂
id                                     └─┘   └┘ └┘    └┘ └┘   └─┘ └┘ └┘
src                                     └─┘    └┘        └┘      └─┘
typ                                    └─┘   └┘ └┘    └┘ └┘   └─┘ └┘ └┘
doc                                     └─┘                       └─┘
162  | []       := iff.rfl
id     └┘          └─────┘
src    └┘          └─────┘
typ    └┘          └─────┘
163  | (p :: L) := by simp [append_append_left_iff L, cons_cons_iff]
id        └┘                └────────────────────┘   └───────────┘
src       └┘          └────┘                       └┘└───────────┘└─
typ       └┘          └────┘└────────────────────┘└┘└───────────┘└─
doc                   └────┘                       └┘             └─
txt                   └────┘                       └┘             └─
par                   └────┘                       └┘             └─
pid                                              └┘             
st                   └───────────────────────────────────────────────
164  
src  
typ  
doc  
txt  
par  
pid  
st   
165  lemma append_append (h₁ : red L₁ L₃) (h₂ : red L₂ L₄) : red (L₁ ++ L₂) (L₃ ++ L₄) :=
id                             └─┘ └┘ └┘        └─┘ └┘ └┘    └─┘  └┘ └┘ └┘   └┘ └┘ └┘
src                            └─┘              └─┘          └─┘     └┘         └┘
typ                            └─┘ └┘ └┘        └─┘ └┘ └┘    └─┘  └┘ └┘ └┘   └┘ └┘ └┘
doc                            └─┘              └─┘          └─┘
166  (refl_trans_gen_lift (λL, L ++ L₂) (assume a b, step.append_right) h₁).trans
id    └─────────────────┘      └┘ └┘             └───────────────┘  └┘ └───┘
src   └─────────────────┘        └┘                  └───────────────┘     └───┘
typ   └─────────────────┘      └┘ └┘             └───────────────┘  └┘ └───┘
167    ((append_append_left_iff _).2 h₂)
id       └────────────────────┘     └┘
src      └────────────────────┘   
typ      └────────────────────┘     └┘
168  
169  lemma to_append_iff : red L (L₁ ++ L₂) ↔ (∃L₃ L₄, L = L₃ ++ L₄ ∧ red L₃ L₁ ∧ red L₄ L₂) :=
id                         └─┘   └┘ └┘ └┘    └┘ └┘   └┘ └┘ └┘  └─┘ └┘ └┘  └─┘ └┘ └┘
src                        └─┘       └┘                   └┘     └─┘        └─┘
typ                        └─┘   └┘ └┘ └┘    └┘ └┘   └┘ └┘ └┘  └─┘ └┘ └┘  └─┘ └┘ └┘
doc                        └─┘                                        └─┘         └─┘
170  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
171    begin
st     └─────
172      generalize eq : L₁ ++ L₂ = L₁₂,
id                       └┘ └┘ └┘
src      └──────────────┘  └┘   
typ      └──────────────┘└┘└┘└┘ 
doc      └──────────────┘       
txt      └──────────────┘       
par      └──────────────┘       
pid                └─┘└┘       
st   ─────────────────────────────────┘└─
173      assume h,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───────────┘└─
174      induction h with L' L₁₂ hLL' h ih generalizing L₁ L₂,
id                 
src      └────────┘ └───────────────────────────────────────┘
typ      └────────┘└───────────────────────────────────────┘
doc      └────────┘ └───────────────────────────────────────┘
txt      └────────┘ └───────────────────────────────────────┘
par      └────────┘ └───────────────────────────────────────┘
pid                └───────────────────┘└─────────────────┘
st   ───────────────────────────────────────────────────────┘└─
175      { exact ⟨_, _, eq.symm, by refl, by refl⟩ },
id                      └─────┘
src        └────┘ └────┘└─────┘└┘  └──┘└┘  └──┘└┘
typ        └────┘ └────┘└─────┘└┘  └──┘└┘  └──┘└┘
doc        └────┘ └────┘       └┘  └──┘└┘  └──┘└┘
txt        └────┘ └────┘       └┘  └──┘└┘  └──┘└┘
par        └────┘ └────┘       └┘  └──┘└┘  └──┘└┘
pid              └────┘       └┘  └─────┘  └────┘
st   ─────┘└──────────────────────┘└───┘└──┘└───┘└┘└┘
176      { cases h with s e a b,
id               
src        └────┘ └───────────┘
typ        └────┘└───────────┘
doc        └────┘ └───────────┘
txt        └────┘ └───────────┘
par        └────┘ └───────────┘
pid              └───────────┘
st   ─────────────────────────┘└─
177        rcases list.append_eq_append_iff.1 eq with ⟨s', rfl, rfl⟩ | ⟨e', rfl, rfl⟩,
id                └───────────────────────┘   └┘
src        └─────┘└───────────────────────┘└─┘└┘└───────────────────────────────────┘
typ        └─────┘└───────────────────────┘└─┘└┘└───────────────────────────────────┘
doc        └─────┘                         └─┘  └───────────────────────────────────┘
txt        └─────┘                         └─┘  └───────────────────────────────────┘
par        └─────┘                         └─┘  └───────────────────────────────────┘
pid                                       └─┘  └───────────────────────────────────┘
st   ───────────────────────────────────────────────────────────────────────────────┘└─
178        { have : L₁ ++ (s' ++ ((a, b) :: (a, bnot b) :: e)) = (L₁ ++ s') ++ ((a, b) :: (a, bnot b) :: e),
id                                                                └┘    └┘                  └──┘      
src          └─────┘            └┘ └┘    └┘     └┘   └─┘        └┘     └┘ └┘   └┘└──┘ └┘   
typ          └─────┘            └┘ └┘    └┘     └┘   └─┘  └┘  └┘└┘     └┘ └┘  └┘└──┘└┘  
doc          └─────┘            └┘ └┘    └┘     └┘   └─┘        └┘     └┘ └┘    └┘     └┘   
txt          └─────┘            └┘ └┘    └┘     └┘   └─┘        └┘     └┘ └┘    └┘     └┘   
par          └─────┘            └┘ └┘    └┘     └┘   └─┘        └┘     └┘ └┘    └┘     └┘   
pid          └───┘└┘            └┘ └┘    └┘     └┘   └─┘        └┘     └┘ └┘    └┘     └┘   
st   ───────┘└────────────────────────────────────────────────────────────────────────────────────────────┘└─
179          { simp },
src            └───┘
typ            └───┘
doc            └───┘
txt            └───┘
par            └───┘
pid                
st   ─────────┘└───┘└┘
180          rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩,
id                  └┘ └──┘
src          └─────┘      └─────────────────────────┘
typ          └─────┘└┘└──┘└─────────────────────────┘
doc          └─────┘      └─────────────────────────┘
txt          └─────┘      └─────────────────────────┘
par          └─────┘      └─────────────────────────┘
pid                      └─────────────────────────┘
st   ────────────────────────────────────────────────┘└─
181          exact ⟨w₁, w₂, rfl, h₁, h₂.tail step.bnot⟩ },
id                  └┘  └┘  └─┘  └┘  └─────┘ └───────┘
src          └────┘   └┘  └┘└─┘└┘  └┘└─────┘└───────┘└┘
typ          └────┘ └┘└┘└┘└┘└─┘└┘└┘└┘└─────┘└───────┘└┘
doc          └────┘   └┘  └┘   └┘  └┘                └┘
txt          └────┘   └┘  └┘   └┘  └┘                └┘
par          └────┘   └┘  └┘   └┘  └┘                └┘
pid                  └┘  └┘   └┘  └┘                
st   ──────────────────────────────────────────────────┘└┘
182        { have : (s ++ ((a, b) :: (a, bnot b) :: e')) ++ L₂ = s ++ ((a, b) :: (a, bnot b) :: (e' ++ L₂)),
id                                                                                └──┘       └┘    └┘
src          └─────┘       └┘ └┘    └┘     └┘    └─┘           └┘ └┘   └┘└──┘ └┘         └┘
typ          └─────┘       └┘ └┘    └┘     └┘    └─┘          └┘ └┘  └┘└──┘└┘   └┘  └┘└┘
doc          └─────┘       └┘ └┘    └┘     └┘    └─┘           └┘ └┘    └┘     └┘         └┘
txt          └─────┘       └┘ └┘    └┘     └┘    └─┘           └┘ └┘    └┘     └┘         └┘
par          └─────┘       └┘ └┘    └┘     └┘    └─┘           └┘ └┘    └┘     └┘         └┘
pid          └───┘└┘       └┘ └┘    └┘     └┘    └─┘           └┘ └┘    └┘     └┘         └┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
183          { simp },
src            └───┘
typ            └───┘
doc            └───┘
txt            └───┘
par            └───┘
pid                
st   ─────────┘└───┘└┘
184          rcases ih this with ⟨w₁, w₂, rfl, h₁, h₂⟩,
id                  └┘ └──┘
src          └─────┘      └─────────────────────────┘
typ          └─────┘└┘└──┘└─────────────────────────┘
doc          └─────┘      └─────────────────────────┘
txt          └─────┘      └─────────────────────────┘
par          └─────┘      └─────────────────────────┘
pid                      └─────────────────────────┘
st   ────────────────────────────────────────────────┘└─
185          exact ⟨w₁, w₂, rfl, h₁.tail step.bnot, h₂⟩ }, }
id                  └┘  └┘  └─┘  └─────┘ └───────┘  └┘
src          └────┘   └┘  └┘└─┘└┘└─────┘└───────┘└┘  └┘
typ          └────┘ └┘└┘└┘└┘└─┘└┘└─────┘└───────┘└┘└┘└┘
doc          └────┘   └┘  └┘   └┘                └┘  └┘
txt          └────┘   └┘  └┘   └┘                └┘  └┘
par          └────┘   └┘  └┘   └┘                └┘  └┘
pid                  └┘  └┘   └┘                └┘  
st   ──────────────────────────────────────────────────┘└────
186    end
st   ────┘
187    (assume ⟨L₃, L₄, eq, h₃, h₄⟩, eq.symm ▸ append_append h₃ h₄)
id                     └┘  └┘  └┘     └───┘  └───────────┘
src                     └┘             └───┘  └───────────┘
typ                    └┘  └┘  └┘     └───┘  └───────────┘
188  
189  /-- The empty word `[]` only reduces to itself. -/
190  theorem nil_iff : red [] L ↔ L = [] :=
id                     └─┘ └┘     └┘
src                    └─┘ └┘       └┘
typ                    └─┘ └┘     └┘
doc                    └─┘
191  refl_trans_gen_iff_eq (assume l, red.not_step_nil)
id   └───────────────────┘           └──────────────┘
src  └───────────────────┘            └──────────────┘
typ  └───────────────────┘           └──────────────┘
192  
193  /-- A letter only reduces to itself. -/
194  theorem singleton_iff {x} : red [x] L₁ ↔ L₁ = [x] :=
id                               └─┘  └┘  └┘  
src                              └─┘            
typ                              └─┘  └┘  └┘  
doc                              └─┘
195  refl_trans_gen_iff_eq (assume l, not_step_singleton)
id   └───────────────────┘           └────────────────┘
src  └───────────────────┘            └────────────────┘
typ  └───────────────────┘           └────────────────┘
196  
197  /-- If `x` is a letter and `w` is a word such that `xw` reduces to the empty word, then `w` reduces
198  to `x⁻¹` -/
199  theorem cons_nil_iff_singleton {x b} : red ((x, b) :: L) [] ↔ red L [(x, bnot b)] :=
id                                          └─┘      └┘   └┘  └─┘    └──┘  
src                                         └─┘        └┘    └┘  └─┘      └──┘   
typ                                         └─┘      └┘   └┘  └─┘    └──┘  
doc                                         └─┘                    └─┘
200  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
201    (assume h,
id             
typ            
202      have h₁ : red ((x, bnot b) :: (x, b) :: L) [(x, bnot b)], from cons_cons h,
id                 └─┘    └──┘   └┘     └┘     └──┘         └───────┘ 
src                └─┘     └──┘    └┘       └┘       └──┘          └───────┘
typ                └─┘    └──┘   └┘     └┘     └──┘         └───────┘ 
doc                └─┘
203      have h₂ : red ((x, bnot b) :: (x, b) :: L) L, from refl_trans_gen.single step.cons_bnot_rev,
id                 └─┘    └──┘   └┘     └┘          └───────────────────┘ └────────────────┘
src                └─┘     └──┘    └┘       └┘            └───────────────────┘ └────────────────┘
typ                └─┘    └──┘   └┘     └┘          └───────────────────┘ └────────────────┘
doc                └─┘
204      let ⟨L', h₁, h₂⟩ := church_rosser h₁ h₂ in
id       └─┘                 └───────────┘ └┘ └┘
src                          └───────────┘
typ      └─┘                 └───────────┘ └┘ └┘
doc                          └───────────┘
205      by rw [singleton_iff] at h₁; subst L'; assumption)
id              └───────────┘               └┘
src         └──┘└───────────┘└─────┘  └────┘    └────────┘
typ         └──┘└───────────┘└─────┘  └────┘└┘  └────────┘
doc         └──┘└───────────┘└─────┘  └────┘    └────────┘
txt         └──┘             └─────┘  └────┘    └────────┘
par         └──┘             └─────┘  └────┘    └────────┘
pid           └┘             └────┘       
st         └────────────────┘└──────────────────────────┘
206    (assume h, (cons_cons h).tail step.cons_bnot)
id                └───────┘  └──┘  └────────────┘
src                └───────┘   └──┘  └────────────┘
typ               └───────┘  └──┘  └────────────┘
207  
208  theorem red_iff_irreducible {x1 b1 x2 b2} (h : (x1, b1) ≠ (x2, b2)) :
id                                                  └┘  └┘   └┘  └┘
src                                                          
typ                                                 └┘  └┘   └┘  └┘
209    red [(x1, bnot b1), (x2, b2)] L ↔ L = [(x1, bnot b1), (x2, b2)] :=
id     └─┘ └┘  └──┘ └┘  └┘  └┘      └┘  └──┘ └┘  └┘  └┘ 
src    └─┘     └──┘                       └──┘            
typ    └─┘ └┘  └──┘ └┘  └┘  └┘      └┘  └──┘ └┘  └┘  └┘ 
doc    └─┘
210  begin
st   └─────
211    apply refl_trans_gen_iff_eq,
id           └───────────────────┘
src    └────┘└───────────────────┘
typ    └────┘└───────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────────────────────────┘└─
212    generalize eq : [(x1, bnot b1), (x2, b2)] = L',
id                      └┘  └──┘ └┘  └┘  └┘ 
src    └──────────────┘   └┘└──┘    └┘   
typ    └──────────────┘ └┘└┘└──┘└┘└┘└┘└┘ 
doc    └──────────────┘    └┘          └┘    
txt    └──────────────┘    └┘          └┘    
par    └──────────────┘    └┘          └┘    
pid              └─┘└┘    └┘          └┘    
st   ───────────────────────────────────────────────┘└─
213    assume L h',
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
214    cases h',
id           └┘
src    └────┘
typ    └────┘└┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────┘└─
215    simp [list.cons_eq_append_iff, list.nil_eq_append_iff] at eq,
id           └─────────────────────┘  └────────────────────┘
src    └────┘└─────────────────────┘└┘└────────────────────┘└─────┘
typ    └────┘└─────────────────────┘└┘└────────────────────┘└─────┘
doc    └────┘                       └┘                      └─────┘
txt    └────┘                       └┘                      └─────┘
par    └────┘                       └┘                      └─────┘
pid                               └┘                      └───┘
st   ─────────────────────────────────────────────────────────────┘└─
216    rcases eq with ⟨rfl, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩, rfl⟩, subst_vars,
id            └┘
src    └─────┘└┘└──────────────────────────────────────┘  └────────┘
typ    └─────┘└┘└──────────────────────────────────────┘  └────────┘
doc    └─────┘  └──────────────────────────────────────┘  └────────┘
txt    └─────┘  └──────────────────────────────────────┘  └────────┘
par    └─────┘  └──────────────────────────────────────┘  └────────┘
pid            └──────────────────────────────────────┘
st   ──────────────────────────────────────────────────┘└─────────────
217    simp at h,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
pid        └──┘
st   ──────────┘└─
218    contradiction
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid                 
st   ───────────────┘
219  end
st   └─┘
220  
221  /-- If `x` and `y` are distinct letters and `w₁ w₂` are words such that `xw₁` reduces to `yw₂`, then
222  `w₁` reduces to `x⁻¹yw₂`. -/
223  theorem inv_of_red_of_ne {x1 b1 x2 b2}
224    (H1 : (x1, b1) ≠ (x2, b2))
id           └┘  └┘   └┘  └┘
src                   
typ          └┘  └┘   └┘  └┘
225    (H2 : red ((x1, b1) :: L₁) ((x2, b2) :: L₂)) :
id           └─┘  └┘  └┘  └┘ └┘   └┘  └┘  └┘ └┘
src          └─┘          └┘              └┘
typ          └─┘  └┘  └┘  └┘ └┘   └┘  └┘  └┘ └┘
doc          └─┘
226    red L₁ ((x1, bnot b1) :: (x2, b2) :: L₂) :=
id     └─┘ └┘  └┘  └──┘ └┘  └┘ └┘  └┘  └┘ └┘
src    └─┘         └──┘     └┘         └┘
typ    └─┘ └┘  └┘  └──┘ └┘  └┘ └┘  └┘  └┘ └┘
doc    └─┘
227  begin
st   └─────
228    have : red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂), from H2,
id            └─┘   └┘  └┘     └┘   └┘  └┘  └┘ └┘        └┘
src    └─────┘└─┘    └┘  └┘    └┘   └┘  └┘    └───┘
typ    └─────┘└─┘  └┘└┘└┘└┘  └┘└┘ └┘└┘└┘└┘└┘  └───┘└┘
doc    └─────┘└─┘    └┘  └┘    └┘     └┘         └───┘
txt    └─────┘       └┘  └┘    └┘     └┘         └───┘
par    └─────┘       └┘  └┘    └┘     └┘         └───┘
pid    └───┘└┘       └┘  └┘    └┘     └┘         └───┘
st   ───────────────────────────────────────────────┘└───────┘└─
229    rcases to_append_iff.1 this with ⟨_ | ⟨p, L₃⟩, L₄, eq, h₁, h₂⟩,
id            └───────────┘   └──┘
src    └─────┘└───────────┘└─┘    └─────────────────────────────────┘
typ    └─────┘└───────────┘└─┘└──┘└─────────────────────────────────┘
doc    └─────┘             └─┘    └─────────────────────────────────┘
txt    └─────┘             └─┘    └─────────────────────────────────┘
par    └─────┘             └─┘    └─────────────────────────────────┘
pid                       └─┘    └─────────────────────────────────┘
st   ───────────────────────────────────────────────────────────────┘└─
230    { simp [nil_iff] at h₁, contradiction },
id             └─────┘
src      └────┘└─────┘└─────┘  └────────────┘
typ      └────┘└─────┘└─────┘  └────────────┘
doc      └────┘└─────┘└─────┘  └────────────┘
txt      └────┘       └─────┘  └────────────┘
par      └────┘       └─────┘  └────────────┘
pid                 └───┘               
st   ───┘└──────────────────┘└──────────────┘└┘
231    { cases eq,
id             └┘
src      └────┘└┘
typ      └────┘└┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───────────┘└─
232      show red (L₃ ++ L₄) ([(x1, bnot b1), (x2, b2)] ++ L₂),
id            └─┘  └┘    └┘    └┘  └──┘ └┘  └┘  └┘     └┘
src      └───┘└─┘       └┘    └┘└──┘    └┘      
typ      └───┘└─┘ └┘  └┘└┘  └┘└┘└──┘└┘└┘└┘└┘  └┘
doc      └───┘└─┘       └┘     └┘          └┘       
txt      └───┘          └┘     └┘          └┘       
par      └───┘          └┘     └┘          └┘       
pid      └───┘          └┘     └┘          └┘       
st   ────────────────────────────────────────────────────────┘└─
233      apply append_append _ h₂,
id             └───────────┘   └┘
src      └────┘└───────────┘└─┘
typ      └────┘└───────────┘└─┘└┘
doc      └────┘             └─┘
txt      └────┘             └─┘
par      └────┘             └─┘
pid                        └─┘
st   ───────────────────────────┘└─
234      have h₁ : red ((x1, bnot b1) :: (x1, b1) :: L₃) [(x1, bnot b1), (x2, b2)],
id                 └─┘                               └┘   └┘  └──┘ └┘  └┘  └┘ 
src      └────────┘└─┘    └┘      └┘     └┘  └┘    └┘   └┘└──┘    └┘  
typ      └────────┘└─┘    └┘      └┘     └┘  └┘  └┘└┘ └┘└┘└──┘└┘└┘└┘└┘
doc      └────────┘└─┘    └┘      └┘     └┘  └┘    └┘    └┘          └┘  
txt      └────────┘       └┘      └┘     └┘  └┘    └┘    └┘          └┘  
par      └────────┘       └┘      └┘     └┘  └┘    └┘    └┘          └┘  
pid      └─────┘└─┘       └┘      └┘     └┘  └┘    └┘    └┘          └┘  
st   ────────────────────────────────────────────────────────────────────────────┘└─
235      { exact cons_cons h₁ },
id               └───────┘ └┘
src        └────┘└───────┘  
typ        └────┘└───────┘└┘
doc        └────┘           
txt        └────┘           
par        └────┘           
pid                        
st   ─────┘└─────────────────┘└┘
236      have h₂ : red ((x1, bnot b1) :: (x1, b1) :: L₃) L₃,
id                 └─┘       └──┘        └┘  └┘         └┘
src      └────────┘└─┘    └┘└──┘  └┘    └┘  └┘    └┘
typ      └────────┘└─┘    └┘└──┘  └┘  └┘└┘└┘└┘    └┘└┘
doc      └────────┘└─┘    └┘      └┘     └┘  └┘    └┘
txt      └────────┘       └┘      └┘     └┘  └┘    └┘
par      └────────┘       └┘      └┘     └┘  └┘    └┘
pid      └─────┘└─┘       └┘      └┘     └┘  └┘    └┘
st   ─────────────────────────────────────────────────────┘└─
237      { exact step.cons_bnot_rev.to_red },
id               └───────────────────────┘
src        └────┘└───────────────────────┘
typ        └────┘└───────────────────────┘
doc        └────┘                         
txt        └────┘                         
par        └────┘                         
pid                                      
st   ─────┘└──────────────────────────────┘└┘
238      rcases church_rosser h₁ h₂ with ⟨L', h₁, h₂⟩,
id              └───────────┘ └┘ └┘
src      └─────┘└───────────┘    └────────────────┘
typ      └─────┘└───────────┘└┘└┘└────────────────┘
doc      └─────┘└───────────┘    └────────────────┘
txt      └─────┘                 └────────────────┘
par      └─────┘                 └────────────────┘
pid                             └────────────────┘
st   ───────────────────────────────────────────────┘└─
239      rw [red_iff_irreducible H1] at h₁,
id           └─────────────────┘ └┘
src      └──┘└─────────────────┘  └─────┘
typ      └──┘└─────────────────┘└┘└─────┘
doc      └──┘                     └─────┘
txt      └──┘                     └─────┘
par      └──┘                     └─────┘
pid        └┘                     └────┘
st   ─────────────────────────────┘└────┘└─
240      rwa [h₁] at h₂ }
id            └┘
src      └───┘  └──────┘
typ      └───┘└┘└──────┘
doc      └───┘  └──────┘
txt      └───┘  └──────┘
par      └───┘  └──────┘
pid         └┘  └────┘
st   ──────────┘└─────┘└─
241  end
st   ──┘
242  
243  theorem step.sublist (H : red.step L₁ L₂) : L₂ <+ L₁ :=
id                             └──────┘ └┘ └┘    └┘ └┘ └┘
src                            └──────┘             └┘
typ                            └──────┘ └┘ └┘    └┘ └┘ └┘
doc                            └──────┘
244  by cases H; simp; constructor; constructor; refl
id            
src     └────┘   └──┘  └─────────┘  └─────────┘  └────
typ     └────┘  └──┘  └─────────┘  └─────────┘  └────
doc     └────┘   └──┘  └─────────┘  └─────────┘  └────
txt     └────┘   └──┘  └─────────┘  └─────────┘  └────
par     └────┘   └──┘  └─────────┘  └─────────┘  └────
pid                                                 
st     └──────────────────────────────────────────────
245  
src  
typ  
doc  
txt  
par  
pid  
st   
246  /-- If `w₁ w₂` are words such that `w₁` reduces to `w₂`, then `w₂` is a sublist of `w₁`. -/
247  theorem sublist : red L₁ L₂ → L₂ <+ L₁ :=
id                     └─┘ └┘ └┘   └┘ └┘ └┘
src                    └─┘            └┘
typ                    └─┘ └┘ └┘   └┘ └┘ └┘
doc                    └─┘
248  refl_trans_gen_of_transitive_reflexive
id   └────────────────────────────────────┘
src  └────────────────────────────────────┘
typ  └────────────────────────────────────┘
249    (λl, list.sublist.refl l) (λa b c hab hbc, list.sublist.trans hbc hab) (λa b, red.step.sublist)
id         └───────────────┘        └─┘ └─┘  └────────────────┘ └─┘ └─┘       └──────────────┘
src         └───────────────┘                     └────────────────┘                 └──────────────┘
typ        └───────────────┘        └─┘ └─┘  └────────────────┘ └─┘ └─┘       └──────────────┘
250  
251  theorem sizeof_of_step : ∀ {L₁ L₂ : list (α × bool)}, step L₁ L₂ → L₂.sizeof < L₁.sizeof
id                                      └──┘    └──┘    └──┘ └┘ └┘   └┘└─────┘  └┘└─────┘
src                                      └──┘     └──┘    └──┘           └─────┘    └─────┘
typ                                     └──┘    └──┘    └──┘ └┘ └┘   └┘└─────┘  └┘└─────┘
doc                                                        └──┘
252  | _ _ (@step.bnot _ L1 L2 x b) :=
id           └───────┘
src          └───────┘
typ          └───────┘
253    begin
st     └─────
254      induction L1 with hd tl ih,
id                 └┘
src      └────────┘  └────────────┘
typ      └────────┘└┘└────────────┘
doc      └────────┘  └────────────┘
txt      └────────┘  └────────────┘
par      └────────┘  └────────────┘
pid                 └───────────┘
st   ─────────────────────────────┘└─
255      case list.nil
src      └─────────────
typ      └─────────────
doc      └─────────────
txt      └─────────────
par      └─────────────
pid          └───────┘
st   ──────────────────
256      { dsimp [list.sizeof],
id                └─────────┘
src  ─────┘└─────┘└─────────┘└─
typ  ─────┘└─────┘└─────────┘└─
doc  ─────┘└─────┘           └─
txt  ─────┘└─────┘           └─
par  ─────┘└─────┘           └─
pid  ───┘└───────┘           └──
st   ────┘└──────────────────┘└─
257        have H : 1 + sizeof (x, b) + (1 + sizeof (x, bnot b) + list.sizeof L2)
id                    
src  ─────┘└─────────┘        └┘ └┘  └┘         └┘     └┘              └─
typ  ─────┘└─────────┘        └┘ └┘  └┘         └┘     └┘              └─
doc  ─────┘└─────────┘         └┘ └┘  └┘         └┘     └┘              └─
txt  ─────┘└─────────┘         └┘ └┘  └┘         └┘     └┘              └─
par  ─────┘└─────────┘         └┘ └┘  └┘         └┘     └┘              └─
pid  ────────────────┘         └┘ └┘  └┘         └┘     └┘              └─
st   ─────────────────────────────────────────────────────────────────────────────
258          = (list.sizeof L2 + 1) + (sizeof (x, b) + sizeof (x, bnot b) + 1),
id             └─────────┘ └┘                         └────┘   └──┘ 
src  ───────┘ └─────────┘   └──┘          └┘ └┘ └────┘ └┘└──┘ └┘ └─┘└─
typ  ───────┘ └─────────┘└┘ └──┘          └┘ └┘ └────┘└┘└──┘└┘ └─┘└─
doc  ───────┘                └──┘          └┘ └┘         └┘     └┘ └─┘└─
txt  ───────┘                └──┘          └┘ └┘         └┘     └┘ └─┘└─
par  ───────┘                └──┘          └┘ └┘         └┘     └┘ └─┘└─
pid  ───────┘                └──┘          └┘ └┘         └┘     └┘ └────
st   ────────────────────────────────────────────────────────────────────────┘└─
259        { ac_refl },
src  ───────┘└──────┘└──
typ  ───────┘└──────┘└──
doc  ───────┘└──────┘└──
txt  ───────┘└──────┘└──
par  ───────┘└──────┘└──
pid  ───────────────────
st   ──────┘└───────┘└─
260        rw H,
id            
src  ─────┘└─┘ └─
typ  ─────┘└─┘└─
doc  ─────┘└─┘ └─
txt  ─────┘└─┘ └─
par  ─────┘└─┘ └─
pid  ────────┘ └─
st   ─────────┘└─
261        exact nat.le_add_right _ _ },
id               └──────────────┘
src  ─────┘└────┘└──────────────┘└───┘
typ  ─────┘└────┘└──────────────┘└───┘
doc  ─────┘└────┘                └───┘
txt  ─────┘└────┘                └───┘
par  ─────┘└────┘                └───┘
pid  ───────────┘                └────┘
st   ────────────────────────────────┘└┘
262      case list.cons
src      └──────────────
typ      └──────────────
doc      └──────────────
txt      └──────────────
par      └──────────────
pid          └────────┘
st   ───────────────────
263      { dsimp [list.sizeof],
id                └─────────┘
src  ─────┘└─────┘└─────────┘└─
typ  ─────┘└─────┘└─────────┘└─
doc  ─────┘└─────┘           └─
txt  ─────┘└─────┘           └─
par  ─────┘└─────┘           └─
pid  ───┘└───────┘           └──
st   ────────────────────────┘└─
264        exact nat.add_lt_add_left ih _ }
id               └─────────────────┘ └┘
src  ─────┘└────┘└─────────────────┘  └─┘└─
typ  ─────┘└────┘└─────────────────┘└┘└─┘└─
doc  ─────┘└────┘                     └─┘└─
txt  ─────┘└────┘                     └─┘└─
par  ─────┘└────┘                     └─┘└─
pid  ───────────┘                     └──┘
st   ────────────────────────────────────┘
265    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
266  
267  theorem length (h : red L₁ L₂) : ∃ n, L₁.length = L₂.length + 2 * n :=
id                       └─┘ └┘ └┘      └┘└─────┘  └┘└─────┘     
src                      └─┘               └─────┘    └─────┘    
typ                      └─┘ └┘ └┘      └┘└─────┘  └┘└─────┘     
doc                      └─┘
268  begin
st   └─────
269    induction h with L₂ L₃ h₁₂ h₂₃ ih,
id               
src    └────────┘ └────────────────────┘
typ    └────────┘└────────────────────┘
doc    └────────┘ └────────────────────┘
txt    └────────┘ └────────────────────┘
par    └────────┘ └────────────────────┘
pid              └───────────────────┘
st   ──────────────────────────────────┘└─
270    { exact ⟨0, rfl⟩ },
id                 └─┘
src      └────┘ └─┘└─┘└┘
typ      └────┘ └─┘└─┘└┘
doc      └────┘ └─┘   └┘
txt      └────┘ └─┘   └┘
par      └────┘ └─┘   └┘
pid            └─┘   
st   ───┘└─────────────┘└┘
271    { rcases ih with ⟨n, eq⟩,
id              └┘
src      └─────┘  └───────────┘
typ      └─────┘└┘└───────────┘
doc      └─────┘  └───────────┘
txt      └─────┘  └───────────┘
par      └─────┘  └───────────┘
pid              └───────────┘
st   ─────────────────────────┘└─
272      existsi (1 + n),
id                   
src      └──────┘ └┘ 
typ      └──────┘ └┘
doc      └──────┘ └┘  
txt      └──────┘ └┘  
par      └──────┘ └┘  
pid              └┘  
st   ──────────────────┘└─
273      simp [mul_add, eq, (step.length h₂₃).symm] }
id             └─────┘  └┘   └─────────┘ └─┘
src      └────┘└─────┘└┘└┘└┘ └─────────┘   └──────┘
typ      └────┘└─────┘└┘└┘└┘ └─────────┘└─┘└──────┘
doc      └────┘       └┘  └┘ └─────────┘   └──────┘
txt      └────┘       └┘  └┘               └──────┘
par      └────┘       └┘  └┘               └──────┘
pid                 └┘  └┘               └─────┘
st   ──────────────────────────────────────────────┘└─
274  end
st   ──┘
275  
276  theorem antisymm (h₁₂ : red L₁ L₂) : red L₂ L₁ → L₁ = L₂ :=
id                           └─┘ └┘ └┘    └─┘ └┘ └┘   └┘  └┘
src                          └─┘          └─┘            
typ                          └─┘ └┘ └┘    └─┘ └┘ └┘   └┘  └┘
doc                          └─┘          └─┘
277  match L₁, h₁₂.cases_head with
id         └┘  └─┘└─────────┘
src               └─────────┘
typ        └┘  └─┘└─────────┘
278  | _,  or.inl rfl            := assume h, rfl
id         └────┘ └─┘                        └─┘
src        └────┘ └─┘                         └─┘
typ        └────┘ └─┘                        └─┘
279  | L₁, or.inr ⟨L₃, h₁₃, h₃₂⟩ := assume h₂₁,
id         └────┘  └┘       └─┘            └─┘
src        └────┘
typ        └────┘  └┘       └─┘            └─┘
280    let ⟨n, eq⟩ := length (h₃₂.trans h₂₁) in
id     └─┘           └────┘     └────┘ └─┘
src                   └────┘     └────┘
typ    └─┘           └────┘     └────┘ └─┘
281    have list.length L₃ + 0 = list.length L₃ + (2 * n + 2),
id          └─────────┘        └─────────┘           
src         └─────────┘        └─────────┘           
typ         └─────────┘        └─────────┘           
282      by simpa [(step.length h₁₃).symm, add_comm, add_assoc] using eq,
id                  └─────────┘ └─┘        └──────┘  └───────┘        └┘
src         └─────┘ └─────────┘   └──────┘└──────┘└┘└───────┘└──────┘└┘
typ         └─────┘ └─────────┘└─┘└──────┘└──────┘└┘└───────┘└──────┘└┘
doc         └─────┘ └─────────┘   └──────┘        └┘         └──────┘
txt         └─────┘               └──────┘        └┘         └──────┘
par         └─────┘               └──────┘        └┘         └──────┘
pid                             └──────┘        └┘         └────┘
st         └───────────────────────────────────────────────────────────┘
283    (nat.no_confusion $ nat.add_left_cancel this)
id      └──────────────┘   └─────────────────┘ └──┘
src     └──────────────┘   └─────────────────┘
typ     └──────────────┘   └─────────────────┘ └──┘
284  end
285  
286  end red
287  
288  theorem equivalence_join_red : equivalence (join (@red α)) :=
id                                  └─────────┘  └──┘   └─┘ 
src                                 └─────────┘  └──┘   └─┘
typ                                 └─────────┘  └──┘   └─┘ 
doc                                                     └─┘
289  equivalence_join_refl_trans_gen $ assume a b c hab hac,
id   └─────────────────────────────┘             └─┘ └─┘
src  └─────────────────────────────┘
typ  └─────────────────────────────┘             └─┘ └─┘
290  (match b, c, red.step.diamond hab hac rfl with
id              └──────────────┘ └─┘ └─┘ └─┘
src               └──────────────┘         └─┘
typ             └──────────────┘ └─┘ └─┘ └─┘
291  | b, _, or.inl rfl           := ⟨b, by refl, by refl⟩
id          └────┘ └─┘
src          └────┘ └─┘                     └──┘     └──┘
typ         └────┘ └─┘                     └──┘     └──┘
doc                                         └──┘     └──┘
txt                                         └──┘     └──┘
par                                         └──┘     └──┘
st                                         └───┘    └───┘
292  | b, c, or.inr ⟨d, hbd, hcd⟩ := ⟨d, refl_gen.single hbd, refl_trans_gen.single hcd⟩
id           └────┘    └─┘  └─┘         └─────────────┘      └───────────────────┘
src          └────┘                      └─────────────┘      └───────────────────┘
typ          └────┘    └─┘  └─┘         └─────────────┘      └───────────────────┘
293  end)
294  
295  theorem join_red_of_step (h : red.step L₁ L₂) : join red L₁ L₂ :=
id                                 └──────┘ └┘ └┘    └──┘ └─┘ └┘ └┘
src                                └──────┘          └──┘ └─┘
typ                                └──────┘ └┘ └┘    └──┘ └─┘ └┘ └┘
doc                                └──────┘               └─┘
296  join_of_single reflexive_refl_trans_gen h.to_red
id   └────────────┘ └──────────────────────┘ └─────┘
src  └────────────┘ └──────────────────────┘  └─────┘
typ  └────────────┘ └──────────────────────┘ └─────┘
297  
298  theorem eqv_gen_step_iff_join_red : eqv_gen red.step L₁ L₂ ↔ join red L₁ L₂ :=
id                                       └─────┘ └──────┘ └┘ └┘  └──┘ └─┘ └┘ └┘
src                                      └─────┘ └──────┘        └──┘ └─┘
typ                                      └─────┘ └──────┘ └┘ └┘  └──┘ └─┘ └┘ └┘
doc                                              └──────┘              └─┘
299  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
300    (assume h,
id             
typ            
301      have eqv_gen (join red) L₁ L₂ := eqv_gen_mono (assume a b, join_red_of_step) h,
id            └─────┘  └──┘ └─┘  └┘ └┘    └──────────┘            └──────────────┘  
src           └─────┘  └──┘ └─┘           └──────────┘              └──────────────┘
typ           └─────┘  └──┘ └─┘  └┘ └┘    └──────────┘            └──────────────┘  
doc                         └─┘
302      (eqv_gen_iff_of_equivalence $ equivalence_join_red).1 this)
id        └────────────────────────┘   └──────────────────┘   └──┘
src       └────────────────────────┘   └──────────────────┘ 
typ       └────────────────────────┘   └──────────────────┘   └──┘
303    (join_of_equivalence (eqv_gen.is_equivalence _) $ assume a b,
id      └─────────────────┘  └────────────────────┘              
src     └─────────────────┘  └────────────────────┘
typ     └─────────────────┘  └────────────────────┘              
304      refl_trans_gen_of_equivalence (eqv_gen.is_equivalence _) eqv_gen.rel)
id       └───────────────────────────┘  └────────────────────┘    └─────────┘
src      └───────────────────────────┘  └────────────────────┘    └─────────┘
typ      └───────────────────────────┘  └────────────────────┘    └─────────┘
305  
306  end free_group
307  
308  /-- The free group over a type, i.e. the words formed by the elements of the type and their formal
309  inverses, quotient by one step reduction. -/
310  def free_group (α : Type u) : Type u :=
311  quot $ @free_group.red.step α
id   └──┘    └─────────────────┘ 
src          └─────────────────┘
typ  └──┘    └─────────────────┘ 
doc          └─────────────────┘
312  
313  namespace free_group
314  
315  variables {α} {L L₁ L₂ L₃ L₄ : list (α × bool)}
id                                  └──┘     └──┘
src                                 └──┘     └──┘
typ                                 └──┘     └──┘
316  
317  def mk (L) : free_group α := quot.mk red.step L
id                └────────┘     └─────┘ └──────┘ 
src               └────────┘              └──────┘
typ               └────────┘     └─────┘ └──────┘ 
doc               └────────┘              └──────┘
318  
319  @[simp] lemma quot_mk_eq_mk : quot.mk red.step L = mk L := rfl
id                                 └─────┘ └──────┘   └┘     └─┘
src                                        └──────┘    └┘      └─┘
typ                                └─────┘ └──────┘   └┘     └─┘
doc    └──┘                                └──────┘
320  
321  @[simp] lemma quot_lift_mk (β : Type v) (f : list (α × bool) → β)
id                                                └──┘    └──┘    
src                                               └──┘     └──┘
typ                                               └──┘    └──┘    
doc    └──┘
322    (H : ∀ L₁ L₂, red.step L₁ L₂ → f L₁ = f L₂) :
id            └┘ └┘  └──────┘ └┘ └┘    └┘   └┘
src                  └──────┘              
typ           └┘ └┘  └──────┘ └┘ └┘    └┘   └┘
doc                  └──────┘
323  quot.lift f H (mk L) = f L := rfl
id   └───────┘    └┘         └─┘
src                 └┘            └─┘
typ  └───────┘    └┘         └─┘
324  
325  @[simp] lemma quot_lift_on_mk (β : Type v) (f : list (α × bool) → β)
id                                                   └──┘    └──┘    
src                                                  └──┘     └──┘
typ                                                  └──┘    └──┘    
doc    └──┘
326    (H : ∀ L₁ L₂, red.step L₁ L₂ → f L₁ = f L₂) :
id            └┘ └┘  └──────┘ └┘ └┘    └┘   └┘
src                  └──────┘              
typ           └┘ └┘  └──────┘ └┘ └┘    └┘   └┘
doc                  └──────┘
327  quot.lift_on (mk L) f H = f L := rfl
id   └──────────┘  └┘           └─┘
src  └──────────┘  └┘                └─┘
typ  └──────────┘  └┘           └─┘
328  
329  instance : has_one (free_group α) := ⟨mk []⟩
id              └─────┘  └────────┘       └┘ └┘
src             └─────┘  └────────┘        └┘ └┘
typ             └─────┘  └────────┘       └┘ └┘
doc                      └────────┘
330  lemma one_eq_mk : (1 : free_group α) = mk [] := rfl
id                          └────────┘    └┘ └┘    └─┘
src                         └────────┘     └┘ └┘    └─┘
typ                         └────────┘    └┘ └┘    └─┘
doc                         └────────┘
331  
332  instance : inhabited (free_group α) := ⟨1⟩
id              └───────┘  └────────┘ 
src             └───────┘  └────────┘
typ             └───────┘  └────────┘ 
doc                        └────────┘
333  
334  instance : has_mul (free_group α) :=
id              └─────┘  └────────┘ 
src             └─────┘  └────────┘
typ             └─────┘  └────────┘ 
doc                      └────────┘
335  ⟨λ x y, quot.lift_on x
id         └──────────┘ 
src          └──────────┘
typ        └──────────┘ 
336      (λ L₁, quot.lift_on y (λ L₂, mk $ L₁ ++ L₂) (λ L₂ L₃ H, quot.sound $ red.step.append_left H))
id          └┘  └──────────┘     └┘  └┘   └┘ └┘ └┘     └┘ └┘   └────────┘   └──────────────────┘ 
src             └──────────┘          └┘      └┘                 └────────┘   └──────────────────┘
typ         └┘  └──────────┘     └┘  └┘   └┘ └┘ └┘     └┘ └┘   └────────┘   └──────────────────┘ 
337      (λ L₁ L₂ H, quot.induction_on y $ λ L₃, quot.sound $ red.step.append_right H)⟩
id          └┘ └┘   └───────────────┘      └┘  └────────┘   └───────────────────┘ 
src                  └───────────────┘           └────────┘   └───────────────────┘
typ         └┘ └┘   └───────────────┘      └┘  └────────┘   └───────────────────┘ 
338  @[simp] lemma mul_mk : mk L₁ * mk L₂ = mk (L₁ ++ L₂) := rfl
id                          └┘ └┘  └┘ └┘  └┘  └┘ └┘ └┘     └─┘
src                         └┘     └┘     └┘     └┘        └─┘
typ                         └┘ └┘  └┘ └┘  └┘  └┘ └┘ └┘     └─┘
doc    └──┘
339  
340  instance : has_inv (free_group α) :=
id              └─────┘  └────────┘ 
src             └─────┘  └────────┘
typ             └─────┘  └────────┘ 
doc                      └────────┘
341  ⟨λx, quot.lift_on x (λ L, mk (L.map $ λ x : α × bool, (x.1, bnot x.2)).reverse)
id       └──────────┘       └┘  └──┘           └──┘     └──┘    └─────┘
src       └──────────┘         └┘   └──┘            └──┘      └──┘     └─────┘
typ      └──────────┘       └┘  └──┘           └──┘     └──┘    └─────┘
342    (assume a b h, quot.sound $ by cases h; simp)⟩
id                 └────────┘            
src                   └────────┘      └────┘   └──┘
typ                └────────┘      └────┘  └──┘
doc                                   └────┘   └──┘
txt                                   └────┘   └──┘
par                                   └────┘   └──┘
pid                                        
st                                   └────────────┘
343  @[simp] lemma inv_mk : (mk L)⁻¹ = mk (L.map $ λ x : α × bool, (x.1, bnot x.2)).reverse := rfl
id                           └┘  └┘  └┘  └──┘           └──┘     └──┘    └─────┘     └─┘
src                          └┘   └┘  └┘   └──┘            └──┘      └──┘     └─────┘     └─┘
typ                          └┘  └┘  └┘  └──┘           └──┘     └──┘    └─────┘     └─┘
doc    └──┘
344  
345  instance : group (free_group α) :=
id              └───┘  └────────┘ 
src             └───┘  └────────┘
typ             └───┘  └────────┘ 
doc                    └────────┘
346  { mul := (*),
id            
src           
typ           
347    one := 1,
348    inv := has_inv.inv,
id            └─────────┘
src           └─────────┘
typ           └─────────┘
349    mul_assoc := by rintros ⟨L₁⟩ ⟨L₂⟩ ⟨L₃⟩; simp,
src                    └────────────────────┘  └──┘
typ                    └────────────────────┘  └──┘
doc                    └────────────────────┘  └──┘
txt                    └────────────────────┘  └──┘
par                    └────────────────────┘  └──┘
pid                           └─────────────┘
st                    └───────────────────────────┘
350    one_mul := by rintros ⟨L⟩; refl,
src                  └─────────┘  └──┘
typ                  └─────────┘  └──┘
doc                  └─────────┘  └──┘
txt                  └─────────┘  └──┘
par                  └─────────┘  └──┘
pid                         └──┘
st                  └────────────────┘
351    mul_one := by rintros ⟨L⟩; simp [one_eq_mk],
id                                      └───────┘
src                  └─────────┘  └────┘└───────┘
typ                  └─────────┘  └────┘└───────┘
doc                  └─────────┘  └────┘         
txt                  └─────────┘  └────┘         
par                  └─────────┘  └────┘         
pid                         └──┘               
st                  └────────────────────────────┘
352    mul_left_inv := by rintros ⟨L⟩; exact (list.rec_on L rfl $
id                                            └─────────┘  └─┘
src                       └─────────┘  └────┘ └─────────┘ └─┘ 
typ                       └─────────┘  └────┘ └─────────┘└─┘ 
doc                       └─────────┘  └────┘                 
txt                       └─────────┘  └────┘                 
par                       └─────────┘  └────┘                 
pid                              └──┘                        
st                       └────────────────────────────────────────
353      λ ⟨x, b⟩ tl ih, eq.trans (quot.sound $ by simp [one_eq_mk]) ih) }
id                       └──────┘  └────────┘            └───────┘
src  ───┘ └┘ └┘ └───────┘└──────┘ └────────┘   └────┘└───────┘└┘  └┘
typ  ───┘ └┘ └┘ └───────┘└──────┘ └────────┘   └────┘└───────┘└┘  └┘
doc  ───┘ └┘ └┘ └───────┘                      └────┘         └┘  └┘
txt  ───┘ └┘ └┘ └───────┘                      └────┘         └┘  └┘
par  ───┘ └┘ └┘ └───────┘                      └────┘         └┘  └┘
pid  ───┘ └┘ └┘ └───────┘                      └─────┘         └─┘  
st   ────────────────────────────────────────────┘└───────────────┘└────┘
354  
355  /-- `of x` is the canonical injection from the type to the free group over that type by sending each
356  element to the equivalence class of the letter that is the element. -/
357  def of (x : α) : free_group α :=
id                   └────────┘ 
src                   └────────┘
typ                  └────────┘ 
doc                   └────────┘
358  mk [(x, tt)]
id   └┘   └┘ 
src  └┘    └┘ 
typ  └┘   └┘ 
359  
360  theorem red.exact : mk L₁ = mk L₂ ↔ join red L₁ L₂ :=
id                       └┘ └┘  └┘ └┘  └──┘ └─┘ └┘ └┘
src                      └┘     └┘     └──┘ └─┘
typ                      └┘ └┘  └┘ └┘  └──┘ └─┘ └┘ └┘
doc                                           └─┘
361  calc (mk L₁ = mk L₂) ↔ eqv_gen red.step L₁ L₂ : iff.intro (quot.exact _) quot.eqv_gen_sound
id         └┘ └┘  └┘ └┘    └─────┘ └──────┘ └┘ └┘   └───────┘  └────────┘    └────────────────┘
src        └┘     └┘       └─────┘ └──────┘         └───────┘  └────────┘    └────────────────┘
typ        └┘ └┘  └┘ └┘    └─────┘ └──────┘ └┘ └┘   └───────┘  └────────┘    └────────────────┘
doc                                 └──────┘
362    ... ↔ join red L₁ L₂ : eqv_gen_step_iff_join_red
id           └──┘ └─┘ └┘ └┘   └───────────────────────┘
src          └──┘ └─┘         └───────────────────────┘
typ          └──┘ └─┘ └┘ └┘   └───────────────────────┘
doc               └─┘
363  
364  /-- The canonical injection from the type to the free group is an injection. -/
365  theorem of.inj {x y : α} (H : of x = of y) : x = y :=
id                                └┘   └┘       
src                                └┘    └┘        
typ                               └┘   └┘       
doc                                └┘     └┘
366  let ⟨L₁, hx, hy⟩ := red.exact.1 H in
id   └─┘                 └───────┘  
src                      └───────┘
typ  └─┘                 └───────┘  
367  by simp [red.singleton_iff] at hx hy; cc
id            └───────────────┘
src     └────┘└───────────────┘└────────┘  └──
typ     └────┘└───────────────┘└────────┘  └──
doc     └────┘└───────────────┘└────────┘  └──
txt     └────┘                 └────────┘  └──
par     └────┘                 └────────┘  └──
pid                          └──────┘    
st     └──────────────────────────────────────
368  
src  
typ  
doc  
txt  
par  
pid  
st   
369  section to_group
370  
371  variables {β : Type v} [group β] (f : α → β) {x y : free_group α}
id                          └───┘                       └────────┘
src                          └───┘                       └────────┘
typ                         └───┘                       └────────┘
doc                                                      └────────┘
372  
373  def to_group.aux : list (α × bool) → β :=
id                      └──┘    └──┘    
src                     └──┘     └──┘
typ                     └──┘    └──┘    
374  λ L, list.prod $ L.map $ λ x, cond x.2 (f x.1) (f x.1)⁻¹
id       └───────┘   └──┘       └──┘            └┘
src       └───────┘    └──┘        └──┘                 └┘
typ      └───────┘   └──┘       └──┘            └┘
doc       └───────┘
375  
376  theorem red.step.to_group {f : α → β} (H : red.step L₁ L₂) :
id                                            └──────┘ └┘ └┘
src                                             └──────┘
typ                                           └──────┘ └┘ └┘
doc                                             └──────┘
377    to_group.aux f L₁ = to_group.aux f L₂ :=
id     └──────────┘  └┘  └──────────┘  └┘
src    └──────────┘       └──────────┘
typ    └──────────┘  └┘  └──────────┘  └┘
378  by cases H with _ _ _ b; cases b; simp [to_group.aux]
id                                         └──────────┘
src     └────┘ └───────────┘  └────┘   └────┘└──────────┘└─
typ     └────┘└───────────┘  └────┘  └────┘└──────────┘└─
doc     └────┘ └───────────┘  └────┘   └────┘            └─
txt     └────┘ └───────────┘  └────┘   └────┘            └─
par     └────┘ └───────────┘  └────┘   └────┘            └─
pid           └───────────┘                          
st     └───────────────────────────────────────────────────
379  
src  
typ  
doc  
txt  
par  
pid  
st   
380  /-- If `β` is a group, then any function from `α` to `β`
381  extends uniquely to a group homomorphism from
382  the free group over `α` to `β` -/
383  def to_group : free_group α → β :=
id                  └────────┘    
src                 └────────┘
typ                 └────────┘    
doc                 └────────┘
384  quot.lift (to_group.aux f) $ λ L₁ L₂ H, red.step.to_group H
id   └───────┘  └──────────┘       └┘ └┘   └───────────────┘ 
src             └──────────┘                 └───────────────┘
typ  └───────┘  └──────────┘       └┘ └┘   └───────────────┘ 
385  
386  variable {f}
387  
388  @[simp] lemma to_group.mk : to_group f (mk L) =
id                               └──────┘   └┘   
src                              └──────┘    └┘    
typ                              └──────┘   └┘   
doc    └──┘                      └──────┘
389    list.prod (L.map $ λ x, cond x.2 (f x.1) (f x.1)⁻¹) :=
id     └───────┘  └──┘       └──┘            └┘
src    └───────┘   └──┘        └──┘                 └┘
typ    └───────┘  └──┘       └──┘            └┘
doc    └───────┘
390  rfl
id   └─┘
src  └─┘
typ  └─┘
391  
392  @[simp] lemma to_group.of {x} : to_group f (of x) = f x :=
id                                   └──────┘   └┘     
src                                  └──────┘    └┘    
typ                                  └──────┘   └┘     
doc    └──┘                          └──────┘    └┘
393  one_mul _
id   └─────┘
src  └─────┘
typ  └─────┘
394  
395  instance to_group.is_group_hom : is_group_hom (to_group f) :=
id                                    └──────────┘  └──────┘ 
src                                   └──────────┘  └──────┘
typ                                   └──────────┘  └──────┘ 
doc                                   └──────────┘  └──────┘
396  { map_mul := by rintros ⟨L₁⟩ ⟨L₂⟩; simp }
src                  └───────────────┘  └───┘
typ                  └───────────────┘  └───┘
doc                  └───────────────┘  └───┘
txt                  └───────────────┘  └───┘
par                  └───────────────┘  └───┘
pid                         └────────┘      
st                  └───────────────────────┘
397  
398  @[simp] lemma to_group.mul : to_group f (x * y) = to_group f x * to_group f y :=
id                                └──────┘        └──────┘    └──────┘  
src                               └──────┘           └──────┘      └──────┘
typ                               └──────┘        └──────┘    └──────┘  
doc    └──┘                       └──────┘             └──────┘       └──────┘
399  is_mul_hom.map_mul _ _ _
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
400  
401  @[simp] lemma to_group.one : to_group f 1 = 1 :=
id                                └──────┘    
src                               └──────┘     
typ                               └──────┘    
doc    └──┘                       └──────┘
402  is_group_hom.map_one _
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
doc  └──────────────────┘
403  
404  @[simp] lemma to_group.inv : to_group f x⁻¹ = (to_group f x)⁻¹ :=
id                                └──────┘  └┘   └──────┘   └┘
src                               └──────┘    └┘   └──────┘     └┘
typ                               └──────┘  └┘   └──────┘   └┘
doc    └──┘                       └──────┘          └──────┘
405  is_group_hom.map_inv _ _
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
doc  └──────────────────┘
406  
407  theorem to_group.unique (g : free_group α → β) [is_group_hom g]
id                                └────────┘       └──────────┘ 
src                               └────────┘         └──────────┘
typ                               └────────┘       └──────────┘ 
doc                               └────────┘         └──────────┘
408    (hg : ∀ x, g (of x) = f x) : ∀{x}, g x = to_group f x :=
id                 └┘                 └──────┘  
src                  └┘                       └──────┘
typ                └┘                 └──────┘  
doc                  └┘                         └──────┘
409  by rintros ⟨L⟩; exact list.rec_on L (is_group_hom.map_one g)
id                         └─────────┘   └──────────────────┘
src     └─────────┘  └────┘└─────────┘  └──────────────────┘ └┘
typ     └─────────┘  └────┘└─────────┘ └──────────────────┘ └┘
doc     └─────────┘  └────┘             └──────────────────┘ └┘
txt     └─────────┘  └────┘                                  └┘
par     └─────────┘  └────┘                                  └┘
pid            └──┘                                         └┘
st     └──────────────────────────────────────────────────────────
410  (λ ⟨x, b⟩ t (ih : g (mk t) = _), bool.rec_on b
id                                 └─────────┘
src    └┘ └┘ └────────┘     └┘└───┘└─────────┘ 
typ    └┘└┘└────────┘     └┘└───┘└─────────┘ 
doc    └┘ └┘ └────────┘     └┘ └───┘            
txt    └┘ └┘ └────────┘     └┘ └───┘            
par    └┘ └┘ └────────┘     └┘ └───┘            
pid    └┘ └┘ └────────┘     └┘ └───┘            
st   ───────────────────────────────────────────────
411    (show g ((of x)⁻¹ * mk t) = to_group f (mk ((x, ff) :: t)),
id                    └┘                            └┘
src  ─┘           └┘   └┘               └┘└┘└┘   └───
typ  ─┘           └┘   └┘              └┘└┘└┘   └───
doc  ─┘                 └┘                └┘  └┘   └───
txt  ─┘                 └┘                └┘  └┘   └───
par  ─┘                 └┘                └┘  └┘   └───
pid  ─┘                 └┘                └┘  └┘   └───
st   ──────────────────────────────────────────────────────────────
412       by simp [is_mul_hom.map_mul g, is_group_hom.map_inv g, hg, ih, to_group, to_group.aux])
id                 └────────────────┘   └──────────────────┘   └┘  └┘  └──────┘  └──────────┘
src  ───────┘└────┘└────────────────┘ └┘└──────────────────┘ └┘  └┘  └┘└──────┘└┘└──────────┘└─
typ  ───────┘└────┘└────────────────┘└┘└──────────────────┘└┘└┘└┘└┘└┘└──────┘└┘└──────────┘└─
doc  ───────┘└────┘                   └┘└──────────────────┘ └┘  └┘  └┘└──────┘└┘            └─
txt  ───────┘└────┘                   └┘                     └┘  └┘  └┘        └┘            └─
par  ───────┘└────┘                   └┘                     └┘  └┘  └┘        └┘            └─
pid  ─────────────┘                   └┘                     └┘  └┘  └┘        └┘            └──
st   ──────┘└──────────────────────────────────────────────────────────────────────────────────┘└─
413    (show g (of x * mk t) = to_group f (mk ((x, tt) :: t)),
id             └┘            └──────┘   └┘      └┘
src  ─┘       └┘     └┘ └──────┘  └┘   └┘└┘└┘   └───
typ  ─┘      └┘     └┘└──────┘ └┘   └┘└┘└┘   └───
doc  ─┘       └┘     └┘ └──────┘       └┘  └┘   └───
txt  ─┘              └┘                └┘  └┘   └───
par  ─┘              └┘                └┘  └┘   └───
pid  ─┘              └┘                └┘  └┘   └───
st   ──────────────────────────────────────────────────────────
414       by simp [is_mul_hom.map_mul g, is_group_hom.map_inv g, hg, ih, to_group, to_group.aux]))
id                 └────────────────┘   └──────────────────┘   └┘  └┘  └──────┘  └──────────┘
src  ───────┘└────┘└────────────────┘ └┘└──────────────────┘ └┘  └┘  └┘└──────┘└┘└──────────┘└──
typ  ───────┘└────┘└────────────────┘└┘└──────────────────┘└┘└┘└┘└┘└┘└──────┘└┘└──────────┘└──
doc  ───────┘└────┘                   └┘└──────────────────┘ └┘  └┘  └┘└──────┘└┘            └──
txt  ───────┘└────┘                   └┘                     └┘  └┘  └┘        └┘            └──
par  ───────┘└────┘                   └┘                     └┘  └┘  └┘        └┘            └──
pid  ─────────────┘                   └┘                     └┘  └┘  └┘        └┘            └─┘
st   ──────┘└──────────────────────────────────────────────────────────────────────────────────┘└──
415  
src  
typ  
doc  
txt  
par  
pid  
st   
416  
src  
typ  
doc  
txt  
par  
pid  
st   
417  theorem to_group.of_eq (x : free_group α) : to_group of x = x :=
id                               └────────┘     └──────┘ └┘   
src                              └────────┘      └──────┘ └┘   
typ                              └────────┘     └──────┘ └┘   
doc                              └────────┘      └──────┘ └┘
418  eq.symm $ to_group.unique id (λ x, rfl)
id   └─────┘   └─────────────┘ └┘      └─┘
src  └─────┘   └─────────────┘ └┘       └─┘
typ  └─────┘   └─────────────┘ └┘      └─┘
419  
420  theorem to_group.range_subset {s : set β} [is_subgroup s] (H : set.range f ⊆ s) :
id                                      └─┘    └─────────┘        └───────┘   
src                                     └─┘     └─────────┘         └───────┘   
typ                                     └─┘    └─────────┘        └───────┘   
doc                                             └─────────┘         └───────┘
421    set.range (to_group f) ⊆ s :=
id     └───────┘  └──────┘    
src    └───────┘  └──────┘    
typ    └───────┘  └──────┘    
doc    └───────┘  └──────┘
422  by rintros _ ⟨⟨L⟩, rfl⟩; exact list.rec_on L (is_submonoid.one_mem s)
id                                  └─────────┘   └──────────────────┘ 
src     └──────────────────┘  └────┘└─────────┘  └──────────────────┘ └┘
typ     └──────────────────┘  └────┘└─────────┘ └──────────────────┘└┘
doc     └──────────────────┘  └────┘                                  └┘
txt     └──────────────────┘  └────┘                                  └┘
par     └──────────────────┘  └────┘                                  └┘
pid            └───────────┘                                         └┘
st     └───────────────────────────────────────────────────────────────────
423  (λ ⟨x, b⟩ tl ih, bool.rec_on b
id                   └─────────┘
src    └┘ └┘ └───────┘└─────────┘ 
typ    └┘ └┘└───────┘└─────────┘ 
doc    └┘ └┘ └───────┘            
txt    └┘ └┘ └───────┘            
par    └┘ └┘ └───────┘            
pid    └┘ └┘ └───────┘            
st   ───────────────────────────────
424      (by simp at ih ⊢; from is_submonoid.mul_mem
id                              └──────────────────┘
src  ───┘   └──────────┘└┘└───┘└──────────────────┘
typ  ───┘   └──────────┘└─────┘└──────────────────┘
doc  ───┘   └──────────┘└┘└───┘                    
txt  ───┘   └──────────┘└┘└───┘                    
par  ───┘   └──────────┘└─────┘                    
pid  ───┘   └──────────────────┘                    
st   ──────┘└────────────────────────────────────────
425        (is_subgroup.inv_mem $ H ⟨x, rfl⟩) ih)
id          └─────────────────┘       └─┘   └┘
src  ─────┘ └─────────────────┘    └┘└─┘└─┘  └─
typ  ─────┘ └─────────────────┘  └┘└─┘└─┘└┘└─
doc  ─────┘                        └┘   └─┘  └─
txt  ─────┘                        └┘   └─┘  └─
par  ─────┘                        └┘   └─┘  └─
pid  ─────┘                        └┘   └─┘  └─
st   ──────────────────────────────────────────┘└─
426      (by simp at ih ⊢; from is_submonoid.mul_mem (H ⟨x, rfl⟩) ih))
id                              └──────────────────┘      └─┘   └┘
src  ───┘   └──────────┘└┘└───┘└──────────────────┘    └┘└─┘└─┘  └──
typ  ───┘   └──────────┘└─────┘└──────────────────┘  └┘└─┘└─┘└┘└──
doc  ───┘   └──────────┘└┘└───┘                        └┘   └─┘  └──
txt  ───┘   └──────────┘└┘└───┘                        └┘   └─┘  └──
par  ───┘   └──────────┘└─────┘                        └┘   └─┘  └──
pid  ───┘   └──────────────────┘                        └┘   └─┘  └┘
st   ──────┘└──────────────────────────────────────────────────────┘└──
427  
src  
typ  
doc  
txt  
par  
pid  
st   
428  theorem to_group.range_eq_closure :
429    set.range (to_group f) = group.closure (set.range f) :=
id     └───────┘  └──────┘    └───────────┘  └───────┘ 
src    └───────┘  └──────┘     └───────────┘  └───────┘
typ    └───────┘  └──────┘    └───────────┘  └───────┘ 
doc    └───────┘  └──────┘      └───────────┘  └───────┘
430  set.subset.antisymm
id   └─────────────────┘
src  └─────────────────┘
typ  └─────────────────┘
431    (to_group.range_subset group.subset_closure)
id      └───────────────────┘ └──────────────────┘
src     └───────────────────┘ └──────────────────┘
typ     └───────────────────┘ └──────────────────┘
432    (group.closure_subset $ λ y ⟨x, hx⟩, ⟨of x, by simpa⟩)
id      └──────────────────┘              └┘
src     └──────────────────┘                 └┘       └───┘
typ     └──────────────────┘              └┘       └───┘
doc                                          └┘       └───┘
txt                                                   └───┘
par                                                   └───┘
st                                                   └────┘
433  
434  end to_group
435  
436  section map
437  
438  variables {β : Type v} (f : α → β) {x y : free_group α}
id                                             └────────┘
src                                            └────────┘
typ                                            └────────┘
doc                                            └────────┘
439  
440  def map.aux (L : list (α × bool)) : list (β × bool) :=
id                    └──┘    └──┘     └──┘    └──┘
src                   └──┘     └──┘     └──┘     └──┘
typ                   └──┘    └──┘     └──┘    └──┘
441  L.map $ λ x, (f x.1, x.2)
id   └──┘           
src   └──┘               
typ  └──┘           
442  
443  /-- Any function from `α` to `β` extends uniquely
444  to a group homomorphism from the free group
445  ver `α` to the free group over `β`. -/
446  def map (x : free_group α) : free_group β :=
id                └────────┘     └────────┘ 
src               └────────┘      └────────┘
typ               └────────┘     └────────┘ 
doc               └────────┘      └────────┘
447  x.lift_on (λ L, mk $ map.aux f L) $
id   └──────┘      └┘   └─────┘  
src   └──────┘       └┘   └─────┘
typ  └──────┘      └┘   └─────┘  
448  λ L₁ L₂ H, quot.sound $ by cases H; simp [map.aux]
id     └┘ └┘   └────────┘                    └─────┘
src             └────────┘      └────┘   └────┘└─────┘└─
typ    └┘ └┘   └────────┘      └────┘  └────┘└─────┘└─
doc                             └────┘   └────┘       └─
txt                             └────┘   └────┘       └─
par                             └────┘   └────┘       └─
pid                                                
st                             └────────────────────────
449  
src  
typ  
doc  
txt  
par  
pid  
st   
450  instance map.is_group_hom : is_group_hom (map f) :=
id                               └──────────┘  └─┘ 
src                              └──────────┘  └─┘
typ                              └──────────┘  └─┘ 
doc                              └──────────┘  └─┘
451  { map_mul := by rintros ⟨L₁⟩ ⟨L₂⟩; simp [map, map.aux] }
id                                            └─┘  └─────┘
src                  └───────────────┘  └────┘└─┘└┘└─────┘└┘
typ                  └───────────────┘  └────┘└─┘└┘└─────┘└┘
doc                  └───────────────┘  └────┘└─┘└┘       └┘
txt                  └───────────────┘  └────┘   └┘       └┘
par                  └───────────────┘  └────┘   └┘       └┘
pid                         └────────┘         └┘       
st                  └──────────────────────────────────────┘
452  
453  variable {f}
454  
455  @[simp] lemma map.mk : map f (mk L) = mk (L.map (λ x, (f x.1, x.2))) :=
id                          └─┘   └┘    └┘  └──┘          
src                         └─┘    └┘     └┘   └──┘              
typ                         └─┘   └┘    └┘  └──┘          
doc    └──┘                 └─┘
456  rfl
id   └─┘
src  └─┘
typ  └─┘
457  
458  @[simp] lemma map.id : map id x = x :=
id                          └─┘ └┘   
src                         └─┘ └┘   
typ                         └─┘ └┘   
doc    └──┘                 └─┘
459  have H1 : (λ (x : α × bool), x) = id := rfl,
id                       └──┘      └┘    └─┘
src                       └──┘       └┘    └─┘
typ                      └──┘      └┘    └─┘
460  by rcases x with ⟨L⟩; simp [H1]
id                              └┘
src     └─────┘ └───────┘  └────┘  └─
typ     └─────┘└───────┘  └────┘└┘└─
doc     └─────┘ └───────┘  └────┘  └─
txt     └─────┘ └───────┘  └────┘  └─
par     └─────┘ └───────┘  └────┘  └─
pid            └───────┘        
st     └─────────────────────────────
461  
src  
typ  
doc  
txt  
par  
pid  
st   
462  @[simp] lemma map.id' : map (λ z, z) x = x := map.id
id                           └─┘              └────┘
src                          └─┘                  └────┘
typ                          └─┘              └────┘
doc    └──┘                  └─┘
463  
464  theorem map.comp {γ : Type w} {f : α → β} {g : β → γ} {x} :
id                                                   
typ                                                  
465    map g (map f x) = map (g ∘ f) x :=
id     └─┘   └─┘     └─┘      
src    └─┘    └─┘       └─┘    
typ    └─┘   └─┘     └─┘      
doc    └─┘    └─┘        └─┘
466  by rcases x with ⟨L⟩; simp
id             
src     └─────┘ └───────┘  └────
typ     └─────┘└───────┘  └────
doc     └─────┘ └───────┘  └────
txt     └─────┘ └───────┘  └────
par     └─────┘ └───────┘  └────
pid            └───────┘      
st     └────────────────────────
467  
src  
typ  
doc  
txt  
par  
pid  
st   
468  @[simp] lemma map.of {x} : map f (of x) = of (f x) := rfl
id                              └─┘   └┘    └┘        └─┘
src                             └─┘    └┘     └┘          └─┘
typ                             └─┘   └┘    └┘        └─┘
doc    └──┘                     └─┘    └┘      └┘
469  
470  @[simp] lemma map.mul : map f (x * y) = map f x * map f y :=
id                           └─┘        └─┘    └─┘  
src                          └─┘           └─┘      └─┘
typ                          └─┘        └─┘    └─┘  
doc    └──┘                  └─┘             └─┘       └─┘
471  is_mul_hom.map_mul _ x y
id   └────────────────┘    
src  └────────────────┘
typ  └────────────────┘    
472  
473  @[simp] lemma map.one : map f 1 = 1 :=
id                           └─┘    
src                          └─┘     
typ                          └─┘    
doc    └──┘                  └─┘
474  is_group_hom.map_one _
id   └──────────────────┘
src  └──────────────────┘
typ  └──────────────────┘
doc  └──────────────────┘
475  
476  @[simp] lemma map.inv : map f x⁻¹ = (map f x)⁻¹ :=
id                           └─┘  └┘   └─┘   └┘
src                          └─┘    └┘   └─┘     └┘
typ                          └─┘  └┘   └─┘   └┘
doc    └──┘                  └─┘          └─┘
477  is_group_hom.map_inv _ x
id   └──────────────────┘   
src  └──────────────────┘
typ  └──────────────────┘   
doc  └──────────────────┘
478  
479  theorem map.unique (g : free_group α → free_group β) [is_group_hom g]
id                           └────────┘    └────────┘    └──────────┘ 
src                          └────────┘     └────────┘     └──────────┘
typ                          └────────┘    └────────┘    └──────────┘ 
doc                          └────────┘     └────────┘     └──────────┘
480    (hg : ∀ x, g (of x) = of (f x)) : ∀{x}, g x = map f x :=
id                 └┘    └┘                └─┘  
src                  └┘     └┘                     └─┘
typ                └┘    └┘                └─┘  
doc                  └┘      └┘                      └─┘
481  by rintros ⟨L⟩; exact list.rec_on L (is_group_hom.map_one g)
id                         └─────────┘   └──────────────────┘
src     └─────────┘  └────┘└─────────┘  └──────────────────┘ └┘
typ     └─────────┘  └────┘└─────────┘ └──────────────────┘ └┘
doc     └─────────┘  └────┘             └──────────────────┘ └┘
txt     └─────────┘  └────┘                                  └┘
par     └─────────┘  └────┘                                  └┘
pid            └──┘                                         └┘
st     └──────────────────────────────────────────────────────────
482  (λ ⟨x, b⟩ t (ih : g (mk t) = map f (mk t)), bool.rec_on b
id                                            └─────────┘
src    └┘ └┘ └────────┘     └┘        └──┘└─────────┘ 
typ    └┘└┘└────────┘     └┘        └──┘└─────────┘ 
doc    └┘ └┘ └────────┘     └┘         └──┘            
txt    └┘ └┘ └────────┘     └┘         └──┘            
par    └┘ └┘ └────────┘     └┘         └──┘            
pid    └┘ └┘ └────────┘     └┘         └──┘            
st   ──────────────────────────────────────────────────────────
483    (show g ((of x)⁻¹ * mk t) = map f ((of x)⁻¹ * mk t),
id                    └┘        
src  ─┘           └┘   └┘                └──
typ  ─┘           └┘   └┘               └──
doc  ─┘                 └┘                └──
txt  ─┘                 └┘                └──
par  ─┘                 └┘                └──
pid  ─┘                 └┘                └──
st   ───────────────────────────────────────────────────────
484       by simp [is_mul_hom.map_mul g, is_group_hom.map_inv g, hg, ih])
id                 └────────────────┘   └──────────────────┘   └┘  └┘
src  ───────┘└────┘└────────────────┘ └┘└──────────────────┘ └┘  └┘  └─
typ  ───────┘└────┘└────────────────┘└┘└──────────────────┘└┘└┘└┘└┘└─
doc  ───────┘└────┘                   └┘└──────────────────┘ └┘  └┘  └─
txt  ───────┘└────┘                   └┘                     └┘  └┘  └─
par  ───────┘└────┘                   └┘                     └┘  └┘  └─
pid  ─────────────┘                   └┘                     └┘  └┘  └──
st   ──────┘└──────────────────────────────────────────────────────────┘└─
485    (show g (of x * mk t) = map f (of x * mk t),
id                           └─┘   └┘     └┘
src  ─┘              └┘ └─┘  └┘  └┘ └──
typ  ─┘             └┘└─┘ └┘  └┘ └──
doc  ─┘              └┘ └─┘  └┘     └──
txt  ─┘              └┘             └──
par  ─┘              └┘             └──
pid  ─┘              └┘             └──
st   ───────────────────────────────────────────────
486       by simp [is_mul_hom.map_mul g, hg, ih]))
id                 └────────────────┘   └┘  └┘
src  ───────┘└────┘└────────────────┘ └┘  └┘  └──
typ  ───────┘└────┘└────────────────┘└┘└┘└┘└┘└──
doc  ───────┘└────┘                   └┘  └┘  └──
txt  ───────┘└────┘                   └┘  └┘  └──
par  ───────┘└────┘                   └┘  └┘  └──
pid  ─────────────┘                   └┘  └┘  └─┘
st   ──────┘└──────────────────────────────────┘└──
487  
src  
typ  
doc  
txt  
par  
pid  
st   
488  /-- Equivalent types give rise to equivalent free groups. -/
489  def free_group_congr {α β} (e : α ≃ β) : free_group α ≃ free_group β :=
id                                         └────────┘   └────────┘ 
src                                          └────────┘    └────────┘
typ                                        └────────┘   └────────┘ 
doc                                          └────────┘    └────────┘
490  ⟨map e, map e.symm,
id    └─┘   └─┘ └───┘
src   └─┘    └─┘  └───┘
typ   └─┘   └─┘ └───┘
doc   └─┘    └─┘
491   λ x, by simp [function.comp, map.comp],
id                 └───────────┘  └──────┘
src           └────┘└───────────┘└┘└──────┘
typ          └────┘└───────────┘└┘└──────┘
doc           └────┘             └┘        
txt           └────┘             └┘        
par           └────┘             └┘        
pid                            └┘        
st           └─────────────────────────────┘
492   λ x, by simp [function.comp, map.comp]⟩
id                 └───────────┘  └──────┘
src           └────┘└───────────┘└┘└──────┘
typ          └────┘└───────────┘└┘└──────┘
doc           └────┘             └┘        
txt           └────┘             └┘        
par           └────┘             └┘        
pid                            └┘        
st           └─────────────────────────────┘
493  
494  theorem map_eq_to_group : map f x = to_group (of ∘ f) x :=
id                             └─┘    └──────┘  └┘    
src                            └─┘      └──────┘  └┘ 
typ                            └─┘    └──────┘  └┘    
doc                            └─┘       └──────┘  └┘
495  eq.symm $ map.unique _ $ λ x, by simp
id   └─────┘   └────────┘       
src  └─────┘   └────────┘             └────
typ  └─────┘   └────────┘            └────
doc                                   └────
txt                                   └────
par                                   └────
pid                                       
st                                   └─────
496  
src  
typ  
doc  
txt  
par  
pid  
st   
497  end map
498  
499  section prod
500  
501  variables [group α] (x y : free_group α)
id              └───┘           └────────┘
src             └───┘           └────────┘
typ             └───┘           └────────┘
doc                             └────────┘
502  
503  /-- If `α` is a group, then any function from `α` to `α`
504  extends uniquely to a homomorphism from the
505  free group over `α` to `α`. This is the multiplicative
506  version of `sum`. -/
507  def prod : α :=
id              
typ             
508  to_group id x
id   └──────┘ └┘ 
src  └──────┘ └┘
typ  └──────┘ └┘ 
doc  └──────┘
509  
510  variables {x y}
511  
512  @[simp] lemma prod_mk :
doc    └──┘
513    prod (mk L) = list.prod (L.map $ λ x, cond x.2 x.1 x.1⁻¹) :=
id     └──┘  └┘    └───────┘  └──┘       └──┘      └┘
src    └──┘  └┘     └───────┘   └──┘        └──┘         └┘
typ    └──┘  └┘    └───────┘  └──┘       └──┘      └┘
doc    └──┘          └───────┘
514  rfl
id   └─┘
src  └─┘
typ  └─┘
515  
516  @[simp] lemma prod.of {x : α} : prod (of x) = x :=
id                                  └──┘  └┘    
src                                  └──┘  └┘    
typ                                 └──┘  └┘    
doc    └──┘                          └──┘  └┘
517  to_group.of
id   └─────────┘
src  └─────────┘
typ  └─────────┘
518  
519  instance prod.is_group_hom : is_group_hom (@prod α _) :=
id                                └──────────┘   └──┘ 
src                               └──────────┘   └──┘
typ                               └──────────┘   └──┘ 
doc                               └──────────┘   └──┘
520  to_group.is_group_hom
id   └───────────────────┘
src  └───────────────────┘
typ  └───────────────────┘
521  
522  @[simp] lemma prod.mul : prod (x * y) = prod x * prod y :=
id                            └──┘       └──┘   └──┘ 
src                           └──┘         └──┘    └──┘
typ                           └──┘       └──┘   └──┘ 
doc    └──┘                   └──┘           └──┘     └──┘
523  to_group.mul
id   └──────────┘
src  └──────────┘
typ  └──────────┘
524  
525  @[simp] lemma prod.one : prod (1:free_group α) = 1 :=
id                            └──┘    └────────┘   
src                           └──┘    └────────┘    
typ                           └──┘    └────────┘   
doc    └──┘                   └──┘    └────────┘
526  to_group.one
id   └──────────┘
src  └──────────┘
typ  └──────────┘
527  
528  @[simp] lemma prod.inv : prod x⁻¹ = (prod x)⁻¹ :=
id                            └──┘ └┘   └──┘  └┘
src                           └──┘  └┘   └──┘   └┘
typ                           └──┘ └┘   └──┘  └┘
doc    └──┘                   └──┘        └──┘
529  to_group.inv
id   └──────────┘
src  └──────────┘
typ  └──────────┘
530  
531  lemma prod.unique (g : free_group α → α) [is_group_hom g]
id                          └────────┘       └──────────┘ 
src                         └────────┘         └──────────┘
typ                         └────────┘       └──────────┘ 
doc                         └────────┘         └──────────┘
532    (hg : ∀ x, g (of x) = x) {x} :
id                 └┘    
src                  └┘    
typ                └┘    
doc                  └┘
533    g x = prod x :=
id        └──┘ 
src         └──┘
typ       └──┘ 
doc          └──┘
534  to_group.unique g hg
id   └─────────────┘  └┘
src  └─────────────┘
typ  └─────────────┘  └┘
535  
536  end prod
537  
538  theorem to_group_eq_prod_map {β : Type v} [group β] {f : α → β} {x} :
id                                              └───┘           
src                                             └───┘
typ                                             └───┘           
539    to_group f x = prod (map f x) :=
id     └──────┘    └──┘  └─┘  
src    └──────┘      └──┘  └─┘
typ    └──────┘    └──┘  └─┘  
doc    └──────┘       └──┘  └─┘
540  eq.symm $ to_group.unique (prod ∘ map f) $ λ _, by simp
id   └─────┘   └─────────────┘  └──┘  └─┘       
src  └─────┘   └─────────────┘  └──┘  └─┘              └────
typ  └─────┘   └─────────────┘  └──┘  └─┘            └────
doc                             └──┘   └─┘              └────
txt                                                     └────
par                                                     └────
pid                                                         
st                                                     └─────
541  
src  
typ  
doc  
txt  
par  
pid  
st   
542  section sum
543  
544  variables [add_group α] (x y : free_group α)
id              └───────┘           └────────┘
src             └───────┘           └────────┘
typ             └───────┘           └────────┘
doc                                 └────────┘
545  
546  /-- If `α` is a group, then any function from `α` to `α`
547  extends uniquely to a homomorphism from the
548  free group over `α` to `α`. This is the additive
549  version of `prod`. -/
550  def sum : α :=
id             
typ            
551  @prod (multiplicative _) _ x
id    └──┘  └────────────┘      
src   └──┘  └────────────┘
typ   └──┘  └────────────┘      
doc   └──┘
552  
553  variables {x y}
554  
555  @[simp] lemma sum_mk :
doc    └──┘
556    sum (mk L) = list.sum (L.map $ λ x, cond x.2 x.1 (-x.1)) :=
id     └─┘  └┘    └──────┘  └──┘       └──┘      
src    └─┘  └┘     └──────┘   └──┘        └──┘         
typ    └─┘  └┘    └──────┘  └──┘       └──┘      
doc    └─┘          └──────┘
557  rfl
id   └─┘
src  └─┘
typ  └─┘
558  
559  @[simp] lemma sum.of {x : α} : sum (of x) = x :=
id                                 └─┘  └┘    
src                                 └─┘  └┘    
typ                                └─┘  └┘    
doc    └──┘                         └─┘  └┘
560  prod.of
id   └─────┘
src  └─────┘
typ  └─────┘
561  
562  instance sum.is_group_hom : is_group_hom (@sum α _) :=
id                               └──────────┘   └─┘ 
src                              └──────────┘   └─┘
typ                              └──────────┘   └─┘ 
doc                              └──────────┘   └─┘
563  prod.is_group_hom
id   └───────────────┘
src  └───────────────┘
typ  └───────────────┘
564  
565  @[simp] lemma sum.mul : sum (x * y) = sum x + sum y :=
id                           └─┘       └─┘   └─┘ 
src                          └─┘         └─┘    └─┘
typ                          └─┘       └─┘   └─┘ 
doc    └──┘                  └─┘           └─┘     └─┘
566  prod.mul
id   └──────┘
src  └──────┘
typ  └──────┘
567  
568  @[simp] lemma sum.one : sum (1:free_group α) = 0 :=
id                           └─┘    └────────┘   
src                          └─┘    └────────┘    
typ                          └─┘    └────────┘   
doc    └──┘                  └─┘    └────────┘
569  prod.one
id   └──────┘
src  └──────┘
typ  └──────┘
570  
571  @[simp] lemma sum.inv : sum x⁻¹ = -sum x :=
id                           └─┘ └┘  └─┘ 
src                          └─┘  └┘  └─┘
typ                          └─┘ └┘  └─┘ 
doc    └──┘                  └─┘        └─┘
572  prod.inv
id   └──────┘
src  └──────┘
typ  └──────┘
573  
574  end sum
575  
576  def free_group_empty_equiv_unit : free_group empty ≃ unit :=
id                                     └────────┘ └───┘  └──┘
src                                    └────────┘ └───┘  └──┘
typ                                    └────────┘ └───┘  └──┘
doc                                    └────────┘        └──┘
577  { to_fun    := λ _, (),
id                      └┘
src                      └┘
typ                     └┘
578    inv_fun   := λ _, 1,
id                    
typ                   
579    left_inv  := by rintros ⟨_ | ⟨⟨⟨⟩, _⟩, _⟩⟩; refl,
src                    └────────────────────────┘  └──┘
typ                    └────────────────────────┘  └──┘
doc                    └────────────────────────┘  └──┘
txt                    └────────────────────────┘  └──┘
par                    └────────────────────────┘  └──┘
pid                           └─────────────────┘
st                    └───────────────────────────────┘
580    right_inv := λ ⟨⟩, rfl }
id                       └─┘
src                      └─┘
typ                      └─┘
581  
582  def free_group_unit_equiv_int : free_group unit ≃ int :=
id                                   └────────┘ └──┘  └─┘
src                                  └────────┘ └──┘  └─┘
typ                                  └────────┘ └──┘  └─┘
doc                                  └────────┘ └──┘ 
583  { to_fun    := λ x, sum $ map (λ _, 1) x,
id                      └─┘   └─┘         
src                      └─┘   └─┘
typ                     └─┘   └─┘         
doc                      └─┘   └─┘
584    inv_fun   := λ x, of () ^ x,
id                      └┘ └┘  
src                      └┘ └┘ 
typ                     └┘ └┘  
doc                      └┘
585    left_inv  := by rintros ⟨L⟩; exact list.rec_on L rfl
id                                        └─────────┘  └─┘
src                    └─────────┘  └────┘└─────────┘ └─┘
typ                    └─────────┘  └────┘└─────────┘└─┘
doc                    └─────────┘  └────┘               
txt                    └─────────┘  └────┘               
par                    └─────────┘  └────┘               
pid                           └──┘                      
st                    └─────────────────────────────────────
586      (λ ⟨⟨⟩, b⟩ tl ih, by cases b; simp [gpow_add] at ih ⊢; rw ih; refl),
id                                         └──────┘              └┘
src  ───┘  └┘└─┘ └───────┘  └────┘ └┘└────┘└──────┘└───────┘└┘└─┘  └┘└──┘
typ  ───┘  └┘└─┘ └───────┘  └────┘└┘└────┘└──────┘└───────┘└┘└─┘└┘└┘└──┘
doc  ───┘  └┘ └─┘ └───────┘  └────┘ └┘└────┘        └───────┘└┘└─┘  └┘└──┘
txt  ───┘  └┘ └─┘ └───────┘  └────┘ └┘└────┘        └───────┘└┘└─┘  └┘└──┘
par  ───┘  └┘ └─┘ └───────┘  └────┘ └┘└────┘        └───────┘└┘└─┘  └┘└──┘
pid  ───┘  └┘ └─┘ └───────┘  └─────┘ └──────┘        └────────────┘  └─────┘
st   ───────────────────────┘└────────────────────────────────────┘└┘└────┘
587    right_inv := λ x, int.induction_on x (by simp)
id                      └──────────────┘ 
src                      └──────────────┘       └──┘
typ                     └──────────────┘      └──┘
doc                                             └──┘
txt                                             └──┘
par                                             └──┘
st                                             └───┘
588      (λ i ih, by simp at ih; simp [gpow_add, ih])
id           └┘                       └──────┘  └┘
src                  └────────┘  └────┘└──────┘└┘  
typ          └┘     └────────┘  └────┘└──────┘└┘└┘
doc                  └────────┘  └────┘        └┘  
txt                  └────────┘  └────┘        └┘  
par                  └────────┘  └────┘        └┘  
pid                      └───┘              └┘  
st                  └──────────────────────────────┘
589      (λ i ih, by simp at ih; simp [gpow_add, ih]) }
id           └┘                       └──────┘  └┘
src                  └────────┘  └────┘└──────┘└┘  
typ          └┘     └────────┘  └────┘└──────┘└┘└┘
doc                  └────────┘  └────┘        └┘  
txt                  └────────┘  └────┘        └┘  
par                  └────────┘  └────┘        └┘  
pid                      └───┘              └┘  
st                  └──────────────────────────────┘
590  
591  section category
592  
593  variables {β : Type u}
594  
595  instance : monad free_group.{u} :=
id              └───┘ └────────┘
src             └───┘ └────────┘
typ             └───┘ └────────┘
doc                   └────────┘
596  { pure := λ α, of,
id                 └┘
src                 └┘
typ                └┘
doc                 └┘
597    map := λ α β, map,
id                 └─┘
src                  └─┘
typ                └─┘
doc                  └─┘
598    bind := λ α β x f, to_group f x }
id                    └──────┘  
src                       └──────┘
typ                   └──────┘  
doc                       └──────┘
599  
600  @[elab_as_eliminator]
doc    └────────────────┘
601  protected theorem induction_on
602    {C : free_group α → Prop}
id          └────────┘ 
src         └────────┘
typ         └────────┘ 
doc         └────────┘
603    (z : free_group α)
id          └────────┘ 
src         └────────┘
typ         └────────┘ 
doc         └────────┘
604    (C1 : C 1)
id           
typ          
605    (Cp : ∀ x, C $ pure x)
id                  └──┘ 
src                   └──┘
typ                 └──┘ 
606    (Ci : ∀ x, C (pure x) → C (pure x)⁻¹)
id                 └──┘       └──┘  └┘
src                  └──┘         └──┘   └┘
typ                └──┘       └──┘  └┘
607    (Cm : ∀ x y, C x → C y → C (x * y)) : C z :=
id                                  
src                                  
typ                                 
608  quot.induction_on z $ λ L, list.rec_on L C1 $ λ ⟨x, b⟩ tl ih,
id   └───────────────┘        └─────────┘  └┘         └┘ └┘
src  └───────────────┘          └─────────┘
typ  └───────────────┘        └─────────┘  └┘         └┘ └┘
609  bool.rec_on b (Cm _ _ (Ci _ $ Cp x) ih) (Cm _ _ (Cp x) ih)
id   └─────────┘    └┘      └┘     └┘    └┘   └┘      └┘    └┘
src  └─────────┘
typ  └─────────┘    └┘      └┘     └┘    └┘   └┘      └┘    └┘
610  
611  @[simp] lemma map_pure (f : α → β) (x : α) : f <$> (pure x : free_group α) = pure (f x) :=
id                                              └─┘  └──┘    └────────┘    └──┘   
src                                                 └─┘  └──┘     └────────┘     └──┘
typ                                             └─┘  └──┘    └────────┘    └──┘   
doc    └──┘                                                       └────────┘
612  map.of
id   └────┘
src  └────┘
typ  └────┘
613  
614  @[simp] lemma map_one (f : α → β) : f <$> (1 : free_group α) = 1 :=
id                                      └─┘      └────────┘   
src                                        └─┘      └────────┘    
typ                                     └─┘      └────────┘   
doc    └──┘                                         └────────┘
615  map.one
id   └─────┘
src  └─────┘
typ  └─────┘
616  
617  @[simp] lemma map_mul (f : α → β) (x y : free_group α) : f <$> (x * y) = f <$> x * f <$> y :=
id                                          └────────┘      └─┘        └─┘    └─┘ 
src                                           └────────┘        └─┘           └─┘      └─┘
typ                                         └────────┘      └─┘        └─┘    └─┘ 
doc    └──┘                                   └────────┘
618  map.mul
id   └─────┘
src  └─────┘
typ  └─────┘
619  
620  @[simp] lemma map_inv (f : α → β) (x : free_group α) : f <$> (x⁻¹) = (f <$> x)⁻¹ :=
id                                        └────────┘      └─┘  └┘     └─┘  └┘
src                                         └────────┘        └─┘   └┘      └─┘   └┘
typ                                       └────────┘      └─┘  └┘     └─┘  └┘
doc    └──┘                                 └────────┘
621  map.inv
id   └─────┘
src  └─────┘
typ  └─────┘
622  
623  @[simp] lemma pure_bind (f : α → free_group β) (x) : pure x >>= f = f x :=
id                                   └────────┘         └──┘  └─┘    
src                                   └────────┘          └──┘   └─┘   
typ                                  └────────┘         └──┘  └─┘    
doc    └──┘                           └────────┘
624  to_group.of
id   └─────────┘
src  └─────────┘
typ  └─────────┘
625  
626  @[simp] lemma one_bind (f : α → free_group β) : 1 >>= f = 1 :=
id                                  └────────┘       └─┘  
src                                  └────────┘        └─┘   
typ                                 └────────┘       └─┘  
doc    └──┘                          └────────┘
627  @@to_group.one _ f
id     └──────────┘   
src    └──────────┘
typ    └──────────┘   
628  
629  @[simp] lemma mul_bind (f : α → free_group β) (x y : free_group α) : x * y >>= f = (x >>= f) * (y >>= f) :=
id                                  └────────┘          └────────┘        └─┘     └─┘      └─┘ 
src                                  └────────┘           └────────┘           └─┘       └─┘        └─┘
typ                                 └────────┘          └────────┘        └─┘     └─┘      └─┘ 
doc    └──┘                          └────────┘           └────────┘
630  to_group.mul
id   └──────────┘
src  └──────────┘
typ  └──────────┘
631  
632  @[simp] lemma inv_bind (f : α → free_group β) (x : free_group α) : x⁻¹ >>= f = (x >>= f)⁻¹ :=
id                                  └────────┘        └────────┘     └┘ └─┘     └─┘  └┘
src                                  └────────┘         └────────┘       └┘ └─┘       └─┘   └┘
typ                                 └────────┘        └────────┘     └┘ └─┘     └─┘  └┘
doc    └──┘                          └────────┘         └────────┘
633  to_group.inv
id   └──────────┘
src  └──────────┘
typ  └──────────┘
634  
635  instance : is_lawful_monad free_group.{u} :=
id              └─────────────┘ └────────┘
src             └─────────────┘ └────────┘
typ             └─────────────┘ └────────┘
doc                             └────────┘
636  { id_map := λ α x, free_group.induction_on x (map_one id) (λ x, map_pure id x)
id                   └─────────────────────┘   └─────┘ └┘       └──────┘ └┘ 
src                    └─────────────────────┘    └─────┘ └┘        └──────┘ └┘
typ                  └─────────────────────┘   └─────┘ └┘       └──────┘ └┘ 
637      (λ x ih, by rw [map_inv, ih]) (λ x y ihx ihy, by rw [map_mul, ihx, ihy]),
id           └┘         └─────┘  └┘        └─┘ └─┘         └─────┘  └─┘  └─┘
src                  └──┘└─────┘└┘                       └──┘└─────┘└┘   └┘   
typ          └┘     └──┘└─────┘└┘└┘       └─┘ └─┘     └──┘└─────┘└┘└─┘└┘└─┘
doc                  └──┘       └┘                       └──┘       └┘   └┘   
txt                  └──┘       └┘                       └──┘       └┘   └┘   
par                  └──┘       └┘                       └──┘       └┘   └┘   
pid                    └┘       └┘                         └┘       └┘   └┘   
st                  └──────────┘└──┘                    └──────────┘└───┘└───┘
638    pure_bind := λ α β x f, pure_bind f x,
id                         └───────┘  
src                            └───────┘
typ                        └───────┘  
639    bind_assoc := λ α β γ x f g, free_group.induction_on x
id                            └─────────────────────┘ 
src                                 └─────────────────────┘
typ                           └─────────────────────┘ 
640      (by iterate 3 { rw one_bind }) (λ x, by iterate 2 { rw pure_bind })
id                          └──────┘                           └───────┘
src          └──────────┘└─┘└──────┘           └──────────┘└─┘└───────┘
typ          └──────────┘└─┘└──────┘          └──────────┘└─┘└───────┘
doc          └──────────┘└─┘                   └──────────┘└─┘         
txt          └──────────┘└─┘                   └──────────┘└─┘         
par          └──────────┘└─┘                   └──────────┘└─┘         
pid                 └─────┘        └┘                  └─────┘         └┘
st          └───────────────────────┘└┘         └────────────────────────┘└┘
641      (λ x ih, by iterate 3 { rw inv_bind }; rw ih)
id           └┘                    └──────┘       └┘
src                  └──────────┘└─┘└──────┘  └─┘
typ          └┘     └──────────┘└─┘└──────┘  └─┘└┘
doc                  └──────────┘└─┘          └─┘
txt                  └──────────┘└─┘          └─┘
par                  └──────────┘└─┘          └─┘
pid                         └─────┘        └┘    
st                  └───────────────────────┘└┘└──┘└┘
642      (λ x y ihx ihy, by iterate 3 { rw mul_bind }; rw [ihx, ihy]),
id            └─┘ └─┘                    └──────┘        └─┘  └─┘
src                         └──────────┘└─┘└──────┘  └──┘   └┘   
typ           └─┘ └─┘     └──────────┘└─┘└──────┘  └──┘└─┘└┘└─┘
doc                         └──────────┘└─┘          └──┘   └┘   
txt                         └──────────┘└─┘          └──┘   └┘   
par                         └──────────┘└─┘          └──┘   └┘   
pid                                └─────┘        └┘    └┘   └┘   
st                         └───────────────────────┘└┘└───┘└─┘└───┘
643    bind_pure_comp_eq_map := λ α β f x, free_group.induction_on x
id                                     └─────────────────────┘ 
src                                        └─────────────────────┘
typ                                    └─────────────────────┘ 
644      (by rw [one_bind, map_one]) (λ x, by rw [pure_bind, map_pure])
id               └──────┘  └─────┘               └───────┘  └──────┘
src          └──┘└──────┘└┘└─────┘           └──┘└───────┘└┘└──────┘
typ          └──┘└──────┘└┘└─────┘          └──┘└───────┘└┘└──────┘
doc          └──┘        └┘                  └──┘         └┘        
txt          └──┘        └┘                  └──┘         └┘        
par          └──┘        └┘                  └──┘         └┘        
pid            └┘        └┘                    └┘         └┘        
st          └───────────┘└───────┘          └────────────┘└────────┘
645      (λ x ih, by rw [inv_bind, map_inv, ih]) (λ x y ihx ihy, by rw [mul_bind, map_mul, ihx, ihy]) }
id           └┘         └──────┘  └─────┘  └┘        └─┘ └─┘         └──────┘  └─────┘  └─┘  └─┘
src                  └──┘└──────┘└┘└─────┘└┘                       └──┘└──────┘└┘└─────┘└┘   └┘   
typ          └┘     └──┘└──────┘└┘└─────┘└┘└┘       └─┘ └─┘     └──┘└──────┘└┘└─────┘└┘└─┘└┘└─┘
doc                  └──┘        └┘       └┘                       └──┘        └┘       └┘   └┘   
txt                  └──┘        └┘       └┘                       └──┘        └┘       └┘   └┘   
par                  └──┘        └┘       └┘                       └──┘        └┘       └┘   └┘   
pid                    └┘        └┘       └┘                         └┘        └┘       └┘   └┘   
st                  └───────────┘└───────┘└──┘                    └───────────┘└───────┘└───┘└───┘
646  
647  end category
648  
649  section reduce
650  
651  variable [decidable_eq α]
id             └──────────┘
src            └──────────┘
typ            └──────────┘
652  
653  /-- The maximal reduction of a word. It is computable
654  iff `α` has decidable equality. -/
655  def reduce (L : list (α × bool)) : list (α × bool) :=
id                   └──┘    └──┘     └──┘    └──┘
src                  └──┘     └──┘     └──┘     └──┘
typ                  └──┘    └──┘     └──┘    └──┘
656  list.rec_on L [] $ λ hd1 tl1 ih,
id   └─────────┘  └┘     └─┘ └─┘ └┘
src  └─────────┘   └┘
typ  └─────────┘  └┘     └─┘ └─┘ └┘
657  list.cases_on ih [hd1] $ λ hd2 tl2,
id   └───────────┘ └┘ └─┘     └─┘ └─┘
src  └───────────┘       
typ  └───────────┘ └┘ └─┘     └─┘ └─┘
658  if hd1.1 = hd2.1 ∧ hd1.2 = bnot hd2.2 then tl2
id      └─┘   └─┘   └─┘   └──┘ └─┘       └─┘
src                       └──┘    
typ     └─┘   └─┘   └─┘   └──┘ └─┘       └─┘
659  else hd1 :: hd2 :: tl2
id        └─┘ └┘ └─┘ └┘ └─┘
src           └┘     └┘
typ       └─┘ └┘ └─┘ └┘ └─┘
660  
661  @[simp] lemma reduce.cons (x) : reduce (x :: L) =
id                                   └────┘   └┘   
src                                  └────┘    └┘    
typ                                  └────┘   └┘   
doc    └──┘                          └────┘
662    list.cases_on (reduce L) [x] (λ hd tl,
id     └───────────┘  └────┘       └┘ └┘
src    └───────────┘  └────┘     
typ    └───────────┘  └────┘       └┘ └┘
doc                   └────┘
663    if x.1 = hd.1 ∧ x.2 = bnot hd.2 then tl
id           └┘      └──┘ └┘       └┘
src                    └──┘   
typ          └┘      └──┘ └┘       └┘
664    else x :: hd :: tl) := rfl
id           └┘ └┘ └┘ └┘     └─┘
src           └┘    └┘        └─┘
typ          └┘ └┘ └┘ └┘     └─┘
665  
666  /-- The first theorem that characterises the function
667  `reduce`: a word reduces to its maximal reduction. -/
668  theorem reduce.red : red L (reduce L) :=
id                        └─┘   └────┘ 
src                       └─┘    └────┘
typ                       └─┘   └────┘ 
doc                       └─┘    └────┘
669  begin
st   └─────
670    induction L with hd1 tl1 ih,
id               
src    └────────┘ └──────────────┘
typ    └────────┘└──────────────┘
doc    └────────┘ └──────────────┘
txt    └────────┘ └──────────────┘
par    └────────┘ └──────────────┘
pid              └─────────────┘
st   ────────────────────────────┘└─
671    case list.nil
src    └─────────────
typ    └─────────────
doc    └─────────────
txt    └─────────────
par    └─────────────
pid        └───────┘
st   ────────────────
672    { constructor },
src  ───┘└──────────┘
typ  ───┘└──────────┘
doc  ───┘└──────────┘
txt  ───┘└──────────┘
par  ───┘└──────────┘
pid  ─┘└─────────────┘
st   ──┘└───────────┘└┘
673    case list.cons
src    └──────────────
typ    └──────────────
doc    └──────────────
txt    └──────────────
par    └──────────────
pid        └────────┘
st   ─────────────────
674    { dsimp,
src  ───┘└───┘└─
typ  ───┘└───┘└─
doc  ───┘└───┘└─
txt  ───┘└───┘└─
par  ───┘└───┘└─
pid  ─┘└────────
st   ────────┘└─
675      revert ih,
src  ───┘└───────┘└─
typ  ───┘└───────┘└─
doc  ───┘└───────┘└─
txt  ───┘└───────┘└─
par  ───┘└───────┘└─
pid  ───────────────
st   ────────────┘└─
676      generalize htl : reduce tl1 = TL,
id                        └────┘ └─┘
src  ───┘└───────────────┘└────┘      └─
typ  ───┘└───────────────┘└────┘└─┘   └─
doc  ───┘└───────────────┘└────┘      └─
txt  ───┘└───────────────┘            └─
par  ───┘└───────────────┘            └─
pid  ────────────────────┘            └─
st   ───────────────────────────────────┘└─
677      intro ih,
src  ───┘└──────┘└─
typ  ───┘└──────┘└─
doc  ───┘└──────┘└─
txt  ───┘└──────┘└─
par  ───┘└──────┘└─
pid  ──────────────
st   ───────────┘└─
678      cases TL with hd2 tl2,
id             └┘
src  ───┘└────┘  └───────────┘└─
typ  ───┘└────┘└┘└───────────┘└─
doc  ───┘└────┘  └───────────┘└─
txt  ───┘└────┘  └───────────┘└─
par  ───┘└────┘  └───────────┘└─
pid  ─────────┘  └──────────────
st   ────────────────────────┘└─
679      case list.nil
src  ──────────────────
typ  ──────────────────
doc  ──────────────────
txt  ──────────────────
par  ──────────────────
pid  ──────────────────
st   ──────────────────
680      { exact red.cons_cons ih },
id               └───────────┘ └┘
src  ─────┘└────┘└───────────┘  └──
typ  ─────┘└────┘└───────────┘└┘└──
doc  ─────┘└────┘               └──
txt  ─────┘└────┘               └──
par  ─────┘└────┘               └──
pid  ───────────┘               └───
st   ────┘└──────────────────────┘└─
681      case list.cons
src  ───────────────────
typ  ───────────────────
doc  ───────────────────
txt  ───────────────────
par  ───────────────────
pid  ───────────────────
st   ───────────────────
682      { dsimp,
src  ─────┘└───┘└─
typ  ─────┘└───┘└─
doc  ─────┘└───┘└─
txt  ─────┘└───┘└─
par  ─────┘└───┘└─
pid  ─────────────
st   ──────────┘└─
683        by_cases h : hd1.fst = hd2.fst ∧ hd1.snd = bnot (hd2.snd),
id                      └─────┘   └─────┘   └─────┘   └──┘  └─────┘
src  ─────┘└───────┘ └─┘└─────┘ └─────┘ └─────┘ └──┘ └─────┘└─
typ  ─────┘└───────┘ └─┘└─────┘ └─────┘ └─────┘ └──┘ └─────┘└─
doc  ─────┘└───────┘ └─┘                                    └─
txt  ─────┘└───────┘ └─┘                                    └─
par  ─────┘└───────┘ └─┘                                    └─
pid  ──────────────┘ └─┘                                    └──
st   ──────────────────────────────────────────────────────────────┘└─
684        { rw [if_pos h],
id               └────┘ 
src  ───────┘└──┘└────┘ └─
typ  ───────┘└──┘└────┘└─
doc  ───────┘└──┘       └─
txt  ───────┘└──┘       └─
par  ───────┘└──┘       └─
pid  ───────────┘       └──
st   ──────┘└───────────┘└──
685          transitivity,
src  ───────┘└──────────┘└─
typ  ───────┘└──────────┘└─
doc  ───────┘└──────────┘└─
txt  ───────┘└──────────┘└─
par  ───────┘└──────────┘└─
pid  ──────────────────────
st   ───────────────────┘└─
686          { exact red.cons_cons ih },
id                   └───────────┘ └┘
src  ─────────┘└────┘└───────────┘  └──
typ  ─────────┘└────┘└───────────┘└┘└──
doc  ─────────┘└────┘               └──
txt  ─────────┘└────┘               └──
par  ─────────┘└────┘               └──
pid  ───────────────┘               └───
st   ────────┘└──────────────────────┘└─
687          { cases hd1, cases hd2, cases h,
id                   └─┘        └─┘        
src  ─────────┘└────┘   └┘└────┘   └┘└────┘ └─
typ  ─────────┘└────┘└─┘└┘└────┘└─┘└┘└────┘└─
doc  ─────────┘└────┘   └┘└────┘   └┘└────┘ └─
txt  ─────────┘└────┘   └┘└────┘   └┘└────┘ └─
par  ─────────┘└────┘   └┘└────┘   └┘└────┘ └─
pid  ───────────────┘   └──────┘   └──────┘ └─
st   ──────────────────┘└─────────┘└───────┘└─
688            dsimp at *, subst_vars,
src  ─────────┘└────────┘└┘└────────┘└─
typ  ─────────┘└────────┘└┘└────────┘└─
doc  ─────────┘└────────┘└┘└────────┘└─
txt  ─────────┘└────────┘└┘└────────┘└─
par  ─────────┘└────────┘└┘└────────┘└─
pid  ──────────────────────────────────
st   ───────────────────┘└──────────┘└─
689            exact red.step.cons_bnot_rev.to_red } },
id                   └───────────────────────────┘
src  ─────────┘└────┘└───────────────────────────┘└────
typ  ─────────┘└────┘└───────────────────────────┘└────
doc  ─────────┘└────┘                             └────
txt  ─────────┘└────┘                             └────
par  ─────────┘└────┘                             └────
pid  ───────────────┘                             └─────
st   ─────────────────────────────────────────────┘└─┘└─
690        { rw [if_neg h],
id               └────┘ 
src  ───────┘└──┘└────┘ └─
typ  ───────┘└──┘└────┘└─
doc  ───────┘└──┘       └─
txt  ───────┘└──┘       └─
par  ───────┘└──┘       └─
pid  ───────────┘       └──
st   ───────────────────┘└──
691          exact red.cons_cons ih } } }
id                 └───────────┘ └┘
src  ───────┘└────┘└───────────┘  └────┘
typ  ───────┘└────┘└───────────┘└┘└────┘
doc  ───────┘└────┘               └────┘
txt  ───────┘└────┘               └────┘
par  ───────┘└────┘               └────┘
pid  ─────────────┘               └────┘
st   ──────────────────────────────┘└─┘
692  end
st   └─┘
693  
694  theorem reduce.not {p : Prop} : ∀ {L₁ L₂ L₃ : list (α × bool)} {x b}, reduce L₁ = L₂ ++ (x, b) :: (x, bnot b) :: L₃ → p
id                                                └──┘    └──┘        └────┘ └┘  └┘ └┘     └┘   └──┘   └┘ └┘   
src                                                └──┘     └──┘          └────┘        └┘       └┘    └──┘    └┘
typ                                               └──┘    └──┘        └────┘ └┘  └┘ └┘     └┘   └──┘   └┘ └┘   
doc                                                                        └────┘
695  | [] L2 L3 _ _ := λ h, by cases L2; injections
id     └┘                           └┘
src    └┘                      └────┘    └─────────┘
typ    └┘                     └────┘└┘  └─────────┘
doc                            └────┘    └─────────┘
txt                            └────┘    └─────────┘
par                            └────┘    └─────────┘
pid                                               
st                            └────────────────────┘
696  | ((x,b)::L1) L2 L3 x' b' := begin
id          └┘
src         └┘
typ         └┘
st                                └─────
697    dsimp,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
698    cases r : reduce L1,
id               └────┘ └┘
src    └────┘ └─┘└────┘
typ    └────┘ └─┘└────┘└┘
doc    └────┘ └─┘└────┘
txt    └────┘ └─┘      
par    └────┘ └─┘      
pid          └─┘      
st   ────────────────────┘└─
699    { dsimp, intro h,
src      └───┘  └─────┘
typ      └───┘  └─────┘
doc      └───┘  └─────┘
txt      └───┘  └─────┘
par      └───┘  └─────┘
pid                  └┘
st   ───┘└───┘└───────┘└─
700      have := congr_arg list.length h,
id               └───────┘ └─────────┘ 
src      └──────┘└───────┘└─────────┘
typ      └──────┘└───────┘└─────────┘
doc      └──────┘                    
txt      └──────┘                    
par      └──────┘                    
pid      └───┘└─┘                    
st   ──────────────────────────────────┘└─
701      simp [-add_comm] at this,
src      └──────────────────────┘
typ      └──────────────────────┘
doc      └──────────────────────┘
txt      └──────────────────────┘
par      └──────────────────────┘
pid          └─────────┘└─────┘
st   ───────────────────────────┘└─
702      exact absurd this dec_trivial },
id             └────┘ └──┘ └─────────┘
src      └────┘└────┘    └─────────┘
typ      └────┘└────┘└──┘└─────────┘
doc      └────┘          └─────────┘
txt      └────┘                     
par      └────┘                     
pid                                
st   ─────────────────────────────────┘└┘
703    cases hd with y c,
id           └┘
src    └────┘  └───────┘
typ    └────┘└┘└───────┘
doc    └────┘  └───────┘
txt    └────┘  └───────┘
par    └────┘  └───────┘
pid           └───────┘
st   ──────────────────┘└─
704    by_cases x = y ∧ b = bnot c; simp [h]; intro H,
id                       └──┘         
src    └───────┘      └──┘   └────┘   └─────┘
typ    └───────┘   └──┘  └────┘  └─────┘
doc    └───────┘             └────┘   └─────┘
txt    └───────┘             └────┘   └─────┘
par    └───────┘             └────┘   └─────┘
pid                                     └┘
st   ───────────────────────────────────────────────┘└─
705    { rw H at r,
id          
src      └─┘ └───┘
typ      └─┘└───┘
doc      └─┘ └───┘
txt      └─┘ └───┘
par      └─┘ └───┘
pid         └───┘
st   ───┘└───────┘└─
706      exact @reduce.not L1 ((y,c)::L2) L3 x' b' r },
id              └────────┘ └┘       └┘  └┘ └┘ └┘ 
src      └────┘                     └┘       
typ      └────┘ └────────┘└┘    └┘└┘└┘└┘└┘
doc      └────┘                     └┘       
txt      └────┘                     └┘       
par      └────┘                     └┘       
pid                                └┘       
st   ───────────────────────────────────────────────┘└┘
707    rcases L2 with _|⟨a, L2⟩,
id            └┘
src    └─────┘  └─────────────┘
typ    └─────┘└┘└─────────────┘
doc    └─────┘  └─────────────┘
txt    └─────┘  └─────────────┘
par    └─────┘  └─────────────┘
pid            └─────────────┘
st   ─────────────────────────┘└─
708    { injections, subst_vars,
src      └────────┘  └────────┘
typ      └────────┘  └────────┘
doc      └────────┘  └────────┘
txt      └────────┘  └────────┘
par      └────────┘  └────────┘
st   ───┘└────────┘└──────────┘└─
709      simp at h, cc },
src      └───────┘  └─┘
typ      └───────┘  └─┘
doc      └───────┘  └─┘
txt      └───────┘  └─┘
par      └───────┘  └─┘
pid          └──┘    
st   ────────────┘└───┘└┘
710    { refine @reduce.not L1 L2 L3 x' b' _,
id               └────────┘ └┘ └┘ └┘ └┘ └┘
src      └─────┘                     └┘
typ      └─────┘ └────────┘└┘└┘└┘└┘└┘└┘
doc      └─────┘                     └┘
txt      └─────┘                     └┘
par      └─────┘                     └┘
pid                                 └┘
st   ──────────────────────────────────────┘└─
711      injection H with _ H,
id                 
src      └────────┘ └───────┘
typ      └────────┘└───────┘
doc      └────────┘ └───────┘
txt      └────────┘ └───────┘
par      └────────┘ └───────┘
pid                └───────┘
st   ───────────────────────┘└─
712      rw [r, H], refl }
id             
src      └──┘ └┘   └───┘
typ      └──┘└┘  └───┘
doc      └──┘ └┘   └───┘
txt      └──┘ └┘   └───┘
par      └──┘ └┘   └───┘
pid        └┘ └┘       
st   ────────┘└─┘└──────┘└─
713  end
st   ──┘
714  
715  /-- The second theorem that characterises the
716  function `reduce`: the maximal reduction of a word
717  only reduces to itself. -/
718  theorem reduce.min (H : red (reduce L₁) L₂) : reduce L₁ = L₂ :=
id                           └─┘  └────┘ └┘  └┘    └────┘ └┘  └┘
src                          └─┘  └────┘           └────┘    
typ                          └─┘  └────┘ └┘  └┘    └────┘ └┘  └┘
doc                          └─┘  └────┘           └────┘
719  begin
st   └─────
720    induction H with L1 L' L2 H1 H2 ih,
id               
src    └────────┘ └─────────────────────┘
typ    └────────┘└─────────────────────┘
doc    └────────┘ └─────────────────────┘
txt    └────────┘ └─────────────────────┘
par    └────────┘ └─────────────────────┘
pid              └────────────────────┘
st   ───────────────────────────────────┘└─
721    { refl },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ───┘└───┘└┘
722    { cases H1 with L4 L5 x b,
id             └┘
src      └────┘  └─────────────┘
typ      └────┘└┘└─────────────┘
doc      └────┘  └─────────────┘
txt      └────┘  └─────────────┘
par      └────┘  └─────────────┘
pid             └─────────────┘
st   ──────────────────────────┘└─
723      exact reduce.not H2 }
id             └────────┘ └┘
src      └────┘└────────┘  
typ      └────┘└────────┘└┘
doc      └────┘            
txt      └────┘            
par      └────┘            
pid                       
st   ───────────────────────┘└─
724  end
st   ──┘
725  
726  /-- `reduce` is idempotent, i.e. the maximal reduction
727  of the maximal reduction of a word is the maximal
728  reduction of the word. -/
729  theorem reduce.idem : reduce (reduce L) = reduce L :=
id                         └────┘  └────┘    └────┘ 
src                        └────┘  └────┘     └────┘
typ                        └────┘  └────┘    └────┘ 
doc                        └────┘  └────┘      └────┘
730  eq.symm $ reduce.min reduce.red
id   └─────┘   └────────┘ └────────┘
src  └─────┘   └────────┘ └────────┘
typ  └─────┘   └────────┘ └────────┘
doc            └────────┘ └────────┘
731  
732  theorem reduce.step.eq (H : red.step L₁ L₂) : reduce L₁ = reduce L₂ :=
id                               └──────┘ └┘ └┘    └────┘ └┘  └────┘ └┘
src                              └──────┘          └────┘     └────┘
typ                              └──────┘ └┘ └┘    └────┘ └┘  └────┘ └┘
doc                              └──────┘          └────┘      └────┘
733  let ⟨L₃, HR13, HR23⟩ := red.church_rosser reduce.red (reduce.red.head H) in
id   └─┘      └──┘  └──┘     └───────────────┘ └────────┘  └────────┘└───┘ 
src                          └───────────────┘ └────────┘  └────────┘└───┘
typ  └─┘      └──┘  └──┘     └───────────────┘ └────────┘  └────────┘└───┘ 
doc                          └───────────────┘ └────────┘  └────────┘
734  (reduce.min HR13).trans (reduce.min HR23).symm
id    └────────┘      └───┘   └────────┘      └──┘
src   └────────┘      └───┘   └────────┘      └──┘
typ   └────────┘      └───┘   └────────┘      └──┘
doc   └────────┘              └────────┘
735  
736  /-- If a word reduces to another word, then they have
737  a common maximal reduction. -/
738  theorem reduce.eq_of_red (H : red L₁ L₂) : reduce L₁ = reduce L₂ :=
id                                 └─┘ └┘ └┘    └────┘ └┘  └────┘ └┘
src                                └─┘          └────┘     └────┘
typ                                └─┘ └┘ └┘    └────┘ └┘  └────┘ └┘
doc                                └─┘          └────┘      └────┘
739  let ⟨L₃, HR13, HR23⟩ := red.church_rosser reduce.red (red.trans H reduce.red) in
id   └─┘      └──┘  └──┘     └───────────────┘ └────────┘  └───────┘  └────────┘
src                          └───────────────┘ └────────┘  └───────┘   └────────┘
typ  └─┘      └──┘  └──┘     └───────────────┘ └────────┘  └───────┘  └────────┘
doc                          └───────────────┘ └────────┘              └────────┘
740  (reduce.min HR13).trans (reduce.min HR23).symm
id    └────────┘      └───┘   └────────┘      └──┘
src   └────────┘      └───┘   └────────┘      └──┘
typ   └────────┘      └───┘   └────────┘      └──┘
doc   └────────┘              └────────┘
741  
742  /-- If two words correspond to the same element in
743  the free group, then they have a common maximal
744  reduction. This is the proof that the function that
745  sends an element of the free group to its maximal
746  reduction is well-defined. -/
747  theorem reduce.sound (H : mk L₁ = mk L₂) : reduce L₁ = reduce L₂ :=
id                             └┘ └┘  └┘ └┘    └────┘ └┘  └────┘ └┘
src                            └┘     └┘       └────┘     └────┘
typ                            └┘ └┘  └┘ └┘    └────┘ └┘  └────┘ └┘
doc                                             └────┘      └────┘
748  let ⟨L₃, H13, H23⟩ := red.exact.1 H in
id   └─┘      └─┘  └─┘     └───────┘  
src                        └───────┘
typ  └─┘      └─┘  └─┘     └───────┘  
749  (reduce.eq_of_red H13).trans (reduce.eq_of_red H23).symm
id    └──────────────┘     └───┘   └──────────────┘     └──┘
src   └──────────────┘     └───┘   └──────────────┘     └──┘
typ   └──────────────┘     └───┘   └──────────────┘     └──┘
doc   └──────────────┘             └──────────────┘
750  
751  /-- If two words have a common maximal reduction,
752  then they correspond to the same element in the free group. -/
753  theorem reduce.exact (H : reduce L₁ = reduce L₂) : mk L₁ = mk L₂ :=
id                             └────┘ └┘  └────┘ └┘    └┘ └┘  └┘ └┘
src                            └────┘     └────┘       └┘     └┘
typ                            └────┘ └┘  └────┘ └┘    └┘ └┘  └┘ └┘
doc                            └────┘      └────┘
754  red.exact.2 ⟨reduce L₂, H ▸ reduce.red, reduce.red⟩
id   └───────┘   └────┘ └┘    └────────┘  └────────┘
src  └───────┘   └────┘        └────────┘  └────────┘
typ  └───────┘   └────┘ └┘    └────────┘  └────────┘
doc               └────┘         └────────┘  └────────┘
755  
756  /-- A word and its maximal reduction correspond to
757  the same element of the free group. -/
758  theorem reduce.self : mk (reduce L) = mk L :=
id                         └┘  └────┘    └┘ 
src                        └┘  └────┘     └┘
typ                        └┘  └────┘    └┘ 
doc                            └────┘
759  reduce.exact reduce.idem
id   └──────────┘ └─────────┘
src  └──────────┘ └─────────┘
typ  └──────────┘ └─────────┘
doc  └──────────┘ └─────────┘
760  
761  /-- If words `w₁ w₂` are such that `w₁` reduces to `w₂`,
762  then `w₂` reduces to the maximal reduction of `w₁`. -/
763  theorem reduce.rev (H : red L₁ L₂) : red L₂ (reduce L₁) :=
id                           └─┘ └┘ └┘    └─┘ └┘  └────┘ └┘
src                          └─┘          └─┘     └────┘
typ                          └─┘ └┘ └┘    └─┘ └┘  └────┘ └┘
doc                          └─┘          └─┘     └────┘
764  (reduce.eq_of_red H).symm ▸ reduce.red
id    └──────────────┘  └──┘   └────────┘
src   └──────────────┘   └──┘   └────────┘
typ   └──────────────┘  └──┘   └────────┘
doc   └──────────────┘           └────────┘
765  
766  /-- The function that sends an element of the free
767  group to its maximal reduction. -/
768  def to_word : free_group α → list (α × bool) :=
id                 └────────┘    └──┘    └──┘
src                └────────┘     └──┘     └──┘
typ                └────────┘    └──┘    └──┘
doc                └────────┘
769  quot.lift reduce $ λ L₁ L₂ H, reduce.step.eq H
id   └───────┘ └────┘     └┘ └┘   └────────────┘ 
src            └────┘              └────────────┘
typ  └───────┘ └────┘     └┘ └┘   └────────────┘ 
doc            └────┘
770  
771  lemma to_word.mk : ∀{x : free_group α}, mk (to_word x) = x :=
id                            └────────┘    └┘  └─────┘    
src                           └────────┘     └┘  └─────┘    
typ                           └────────┘    └┘  └─────┘    
doc                           └────────┘         └─────┘
772  by rintros ⟨L⟩; exact reduce.self
id                         └─────────┘
src     └─────────┘  └────┘└─────────┘
typ     └─────────┘  └────┘└─────────┘
doc     └─────────┘  └────┘└─────────┘
txt     └─────────┘  └────┘           
par     └─────────┘  └────┘           
pid            └──┘                  
st     └───────────────────────────────
773  
src  
typ  
doc  
txt  
par  
pid  
st   
774  lemma to_word.inj : ∀(x y : free_group α), to_word x = to_word y → x = y :=
id                               └────────┘    └─────┘   └─────┘      
src                              └────────┘     └─────┘    └─────┘       
typ                              └────────┘    └─────┘   └─────┘      
doc                              └────────┘     └─────┘     └─────┘
775  by rintros ⟨L₁⟩ ⟨L₂⟩; exact reduce.exact
id                               └──────────┘
src     └───────────────┘  └────┘└──────────┘
typ     └───────────────┘  └────┘└──────────┘
doc     └───────────────┘  └────┘└──────────┘
txt     └───────────────┘  └────┘            
par     └───────────────┘  └────┘            
pid            └────────┘                   
st     └──────────────────────────────────────
776  
src  
typ  
doc  
txt  
par  
pid  
st   
777  /-- Constructive Church-Rosser theorem (compare `church_rosser`). -/
778  def reduce.church_rosser (H12 : red L₁ L₂) (H13 : red L₁ L₃) :
id                                   └─┘ └┘ └┘         └─┘ └┘ └┘
src                                  └─┘               └─┘
typ                                  └─┘ └┘ └┘         └─┘ └┘ └┘
doc                                  └─┘               └─┘
779    { L₄ // red L₂ L₄ ∧ red L₃ L₄ } :=
id      └┘    └─┘ └┘ └┘  └─┘ └┘ └┘
src           └─┘        └─┘
typ     └┘    └─┘ └┘ └┘  └─┘ └┘ └┘
doc            └─┘         └─┘
780  ⟨reduce L₁, reduce.rev H12, reduce.rev H13⟩
id    └────┘ └┘  └────────┘ └─┘  └────────┘ └─┘
src   └────┘     └────────┘      └────────┘
typ   └────┘ └┘  └────────┘ └─┘  └────────┘ └─┘
doc   └────┘     └────────┘      └────────┘
781  
782  instance : decidable_eq (free_group α) :=
id              └──────────┘  └────────┘ 
src             └──────────┘  └────────┘
typ             └──────────┘  └────────┘ 
doc                           └────────┘
783  function.injective.decidable_eq to_word.inj
id   └─────────────────────────────┘ └─────────┘
src  └─────────────────────────────┘ └─────────┘
typ  └─────────────────────────────┘ └─────────┘
784  
785  instance red.decidable_rel : decidable_rel (@red α)
id                                └───────────┘   └─┘ 
src                               └───────────┘   └─┘
typ                               └───────────┘   └─┘ 
doc                                               └─┘
786  | [] []          := is_true red.refl
id     └┘ └┘             └─────┘ └──────┘
src    └┘ └┘             └─────┘ └──────┘
typ    └┘ └┘             └─────┘ └──────┘
787  | [] (hd2::tl2)  := is_false $ λ H, list.no_confusion (red.nil_iff.1 H)
id     └┘     └┘         └──────┘       └───────────────┘  └─────────┘  
src    └┘     └┘         └──────┘        └───────────────┘  └─────────┘
typ    └┘     └┘         └──────┘       └───────────────┘  └─────────┘  
doc                                                         └─────────┘
788  | ((x,b)::tl) [] := match red.decidable_rel tl [(x, bnot b)] with
id        └┘└┘  └┘          └───────────────┘       └──┘   
src         └┘    └┘                                  └──┘   
typ       └┘└┘  └┘          └───────────────┘       └──┘   
789    | is_true H  := is_true $ red.trans (red.cons_cons H) $
id       └─────┘      └─────┘   └───────┘  └───────────┘
src      └─────┘       └─────┘   └───────┘  └───────────┘
typ      └─────┘      └─────┘   └───────┘  └───────────┘
790      (@red.step.bnot _ [] [] _ _).to_red
id         └───────────┘   └┘ └┘     └────┘
src        └───────────┘   └┘ └┘     └────┘
typ        └───────────┘   └┘ └┘     └────┘
791    | is_false H := is_false $ λ H2, H $ red.cons_nil_iff_singleton.1 H2
id       └──────┘     └──────┘     └┘      └────────────────────────┘  └┘
src      └──────┘      └──────┘             └────────────────────────┘
typ      └──────┘     └──────┘     └┘      └────────────────────────┘  └┘
doc                                         └────────────────────────┘
792    end
793  | ((x1,b1)::tl1) ((x2,b2)::tl2) := if h : (x1, b1) = (x2, b2)
id      └┘ └┘ └┘└─┘   └┘ └┘ └┘└─┘     └┘              
src           └┘            └┘        └┘              
typ     └┘ └┘ └┘└─┘   └┘ └┘ └┘└─┘     └┘              
794    then match red.decidable_rel tl1 tl2 with
id                └───────────────┘
typ               └───────────────┘
795      | is_true H  := is_true $ h ▸ red.cons_cons H
id         └─────┘      └─────┘     └───────────┘
src        └─────┘       └─────┘      └───────────┘
typ        └─────┘      └─────┘     └───────────┘
796      | is_false H := is_false $ λ H2, H $ h ▸ (red.cons_cons_iff _).1 $ H2
id         └──────┘     └──────┘     └┘         └───────────────┘       └┘
src        └──────┘      └──────┘                 └───────────────┘   
typ        └──────┘     └──────┘     └┘         └───────────────┘       └┘
797      end
798    else match red.decidable_rel tl1 ((x1,bnot b1)::(x2,b2)::tl2) with
id          └───┘ └───────────────┘         └──┘    └┘      └┘
src         └───┘                           └──┘    └┘      └┘
typ         └───┘ └───────────────┘         └──┘    └┘      └┘
799      | is_true H  := is_true $ (red.cons_cons H).tail red.step.cons_bnot
id         └─────┘      └─────┘    └───────────┘   └──┘  └────────────────┘
src        └─────┘       └─────┘    └───────────┘   └──┘  └────────────────┘
typ        └─────┘      └─────┘    └───────────┘   └──┘  └────────────────┘
800      | is_false H := is_false $ λ H2, H $ red.inv_of_red_of_ne h H2
id         └──────┘     └──────┘     └┘      └──────────────────┘  └┘
src        └──────┘      └──────┘             └──────────────────┘
typ        └──────┘     └──────┘     └┘      └──────────────────┘  └┘
doc                                           └──────────────────┘
801      end
802  
803  /-- A list containing every word that `w₁` reduces to. -/
804  def red.enum (L₁ : list (α × bool)) : list (list (α × bool)) :=
id                      └──┘    └──┘     └──┘  └──┘    └──┘
src                     └──┘     └──┘     └──┘  └──┘     └──┘
typ                     └──┘    └──┘     └──┘  └──┘    └──┘
805  list.filter (λ L₂, red L₁ L₂) (list.sublists L₁)
id   └─────────┘    └┘  └─┘ └┘ └┘   └───────────┘ └┘
src  └─────────┘        └─┘         └───────────┘
typ  └─────────┘    └┘  └─┘ └┘ └┘   └───────────┘ └┘
doc                     └─┘         └───────────┘
806  
807  theorem red.enum.sound (H : L₂ ∈ red.enum L₁) : red L₁ L₂ :=
id                               └┘  └──────┘ └┘    └─┘ └┘ └┘
src                                  └──────┘       └─┘
typ                              └┘  └──────┘ └┘    └─┘ └┘ └┘
doc                                   └──────┘       └─┘
808  list.of_mem_filter H
id   └────────────────┘ 
src  └────────────────┘
typ  └────────────────┘ 
809  
810  theorem red.enum.complete (H : red L₁ L₂) : L₂ ∈ red.enum L₁ :=
id                                  └─┘ └┘ └┘    └┘  └──────┘ └┘
src                                 └─┘              └──────┘
typ                                 └─┘ └┘ └┘    └┘  └──────┘ └┘
doc                                 └─┘               └──────┘
811  list.mem_filter_of_mem (list.mem_sublists.2 $ red.sublist H) H
id   └────────────────────┘  └───────────────┘    └─────────┘   
src  └────────────────────┘  └───────────────┘    └─────────┘
typ  └────────────────────┘  └───────────────┘    └─────────┘   
doc                                                └─────────┘
812  
813  instance : fintype { L₂ // red L₁ L₂ } :=
id              └─────┘  └┘    └─┘ └┘ └┘
src             └─────┘        └─┘
typ             └─────┘  └┘    └─┘ └┘ └┘
doc             └─────┘         └─┘
814  fintype.subtype (list.to_finset $ red.enum L₁) $
id   └─────────────┘  └────────────┘   └──────┘ └┘
src  └─────────────┘  └────────────┘   └──────┘
typ  └─────────────┘  └────────────┘   └──────┘ └┘
doc                   └────────────┘   └──────┘
815  λ L₂, ⟨λ H, red.enum.sound $ list.mem_to_finset.1 H,
id     └┘       └────────────┘   └────────────────┘  
src              └────────────┘   └────────────────┘
typ    └┘       └────────────┘   └────────────────┘  
816    λ H, list.mem_to_finset.2 $ red.enum.complete H⟩
id         └────────────────┘    └───────────────┘ 
src         └────────────────┘    └───────────────┘
typ        └────────────────┘    └───────────────┘ 
817  
818  end reduce
819  
820  end free_group